harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean
theorem tag_biUnionTagged (π : Prepartition I) {πi : ∀ J, TaggedPrepartition J} (hJ : J ∈ π) {J'}
    (hJ' : J' ∈ πi J) : (π.biUnionTagged πi).tag J' = (πi J).tag J'

Proof state:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ (π.biUnionTagged πi).tag J' = (πi (π.biUnionIndex (fun J => (πi J).toPrepartition) J')).tag J'

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ (π.biUnionTagged πi).tag J' = (πi J).tag J'

Tactic:
rw [← π.biUnionIndex_of_mem (πi := fun J => (πi J).toPrepartition) hJ hJ']

Result:
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ (π.biUnionTagged πi).tag J' = (πi (π.biUnionIndex (fun J => (πi J).toPrepartition) J')).tag J'
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
theorem Pi.reindex_hom_π (b : β) : (Pi.reindex ε f).hom ≫ Pi.π f (ε b) = Pi.π (f ∘ ε) b

Proof state:
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst✝¹ : HasProduct f
inst✝ : HasProduct (f ∘ ⇑ε)
b : β
⊢ limit.π (Discrete.functor (f ∘ ⇑ε)) { as := ε.symm (ε b) } ≫
      (Discrete.functor f).map ((Discrete.equivalence ε).counit.app { as := ε b }) =
    π (f ∘ ⇑ε) b

Tactic:
exact limit.w (Discrete.functor (f ∘ ε)) (Discrete.eqToHom' (ε.symm_apply_apply b))

Result:
no goals

Proof state:
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst✝¹ : HasProduct f
inst✝ : HasProduct (f ∘ ⇑ε)
b : β
⊢ (HasLimit.isoOfEquivalence (Discrete.equivalence ε) (Discrete.natIso fun x => Iso.refl (f (ε x.as)))).hom ≫
      π f (ε b) =
    π (f ∘ ⇑ε) b

Tactic:
simp only [HasLimit.isoOfEquivalence_hom_π, Discrete.equivalence_inverse, Discrete.functor_obj,
  Function.comp_apply, Functor.id_obj, Discrete.equivalence_functor, Functor.comp_obj,
  Discrete.natIso_inv_app, Iso.refl_inv, Category.id_comp]

Result:
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst✝¹ : HasProduct f
inst✝ : HasProduct (f ∘ ⇑ε)
b : β
⊢ limit.π (Discrete.functor (f ∘ ⇑ε)) { as := ε.symm (ε b) } ≫
      (Discrete.functor f).map ((Discrete.equivalence ε).counit.app { as := ε b }) =
    π (f ∘ ⇑ε) b

Proof state:
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst✝¹ : HasProduct f
inst✝ : HasProduct (f ∘ ⇑ε)
b : β
⊢ (reindex ε f).hom ≫ π f (ε b) = π (f ∘ ⇑ε) b

Tactic:
dsimp [Pi.reindex]

Result:
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst✝¹ : HasProduct f
inst✝ : HasProduct (f ∘ ⇑ε)
b : β
⊢ (HasLimit.isoOfEquivalence (Discrete.equivalence ε) (Discrete.natIso fun x => Iso.refl (f (ε x.as)))).hom ≫
      π f (ε b) =
    π (f ∘ ⇑ε) b
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma Y_ne_negY_of_Y_ne' [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P)
    (hQ : W'.Equation Q) (hx : P x * Q z ^ 2 = Q x * P z ^ 2)
    (hy : P y * Q z ^ 3 ≠ W'.negY Q * P z ^ 3) : P y ≠ W'.negY P

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy' : P y * Q z ^ 3 - Q y * P z ^ 3 = 0
hy : P y = W'.negY P
⊢ P y * Q z ^ 3 = W'.negY Q * P z ^ 3

Tactic:
linear_combination (norm := ring1) Y_sub_Y_add_Y_sub_negY hx + Q z ^ 3 * hy - hy'

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ W'.negY Q * P z ^ 3
⊢ P y ≠ W'.negY P

Tactic:
have hy' : P y * Q z ^ 3 - Q y * P z ^ 3 = 0 :=
  (mul_eq_zero.mp <| Y_sub_Y_mul_Y_sub_negY hP hQ hx).resolve_right <| sub_ne_zero_of_ne hy

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ W'.negY Q * P z ^ 3
hy' : P y * Q z ^ 3 - Q y * P z ^ 3 = 0
⊢ P y ≠ W'.negY P

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ W'.negY Q * P z ^ 3
hy' : P y * Q z ^ 3 - Q y * P z ^ 3 = 0
⊢ P y ≠ W'.negY P

Tactic:
contrapose! hy

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy' : P y * Q z ^ 3 - Q y * P z ^ 3 = 0
hy : P y = W'.negY P
⊢ P y * Q z ^ 3 = W'.negY Q * P z ^ 3
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_nonneg (f : PadicSeq p) : 0 ≤ f.norm

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ 0 ≤ f.norm

Tactic:
simp [norm, hf, padicNorm.nonneg]

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : f ≈ 0
⊢ 0 ≤ f.norm

Tactic:
simp [hf, norm]

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
⊢ 0 ≤ f.norm

Tactic:
exact if hf : f ≈ 0 then by simp [hf, norm] else by simp [norm, hf, padicNorm.nonneg]

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
⊢ 0 ≤ f.norm

Tactic:
classical exact if hf : f ≈ 0 then by simp [hf, norm] else by simp [norm, hf, padicNorm.nonneg]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/SingleFunctors.lean
lemma shiftIso_add'_hom_app (n m mn : A) (hnm : m + n = mn) (a a' a'' : A)
    (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) :
    (F.shiftIso mn a a'' (by rw [← hnm, ← ha'', ← ha', add_assoc])).hom.app X =
      (shiftFunctorAdd' D m n mn hnm).hom.app ((F.functor a'').obj X) ≫
        ((F.shiftIso m a' a'' ha'').hom.app X)⟦n⟧' ≫ (F.shiftIso n a a' ha').hom.app X

Proof state:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst✝⁷ : Category.{?u.16890, u_1} C
inst✝⁶ : Category.{?u.16894, u_2} D
inst✝⁵ : Category.{?u.16898, u_3} E
inst✝⁴ : Category.{?u.16902, u_4} E'
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift D A
inst✝¹ : HasShift E A
inst✝ : HasShift E' A
F G H : SingleFunctors C D A
n m mn : A
hnm : m + n = mn
a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ mn + a = a''

Tactic:
rw [← hnm, ← ha'', ← ha', add_assoc]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_7, u_1} C
inst✝² : Category.{u_6, u_2} D
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : SingleFunctors C D A
n m mn : A
hnm : m + n = mn
a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (F.shiftIso mn a a'' ⋯).hom.app X =
    (shiftFunctorAdd' D m n mn hnm).hom.app ((F.functor a'').obj X) ≫
      (shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').hom.app X) ≫ (F.shiftIso n a a' ha').hom.app X

Tactic:
simp [F.shiftIso_add' n m mn hnm a a' a'' ha' ha'']

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem edist_equiv_symm_snd (y₁ y₂ : β) :
    edist ((WithLp.equiv p (α × β)).symm (0, y₁)) ((WithLp.equiv p (α × β)).symm (0, y₂)) =
      edist y₁ y₂

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
y₁ y₂ : β
⊢ edist ((WithLp.equiv p (α × β)).symm (0, y₁)) ((WithLp.equiv p (α × β)).symm (0, y₂)) = edist y₁ y₂

Tactic:
simp only [edist_nndist, nndist_equiv_symm_snd p α β y₁ y₂]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Module.lean
theorem ContinuousLinearEquiv.map_tsum [T2Space M] [T2Space M₂] {f : ι → M}
    (e : M ≃SL[σ] M₂) : e (∑' z, f z) = ∑' z, e (f z)

Proof state:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
⊢ e (∑' (z : ι), f z) = ∑' (z : ι), e (f z)

Tactic:
refine symm (e.tsum_eq_iff.mpr ?_)

Result:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
⊢ ∑' (z : ι), f z = e.symm (e (∑' (z : ι), f z))

Proof state:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
⊢ ∑' (z : ι), f z = e.symm (e (∑' (z : ι), f z))

Tactic:
rw [e.symm_apply_apply _]

Result:
no goals
-- Mathlib/Topology/Algebra/ConstMulAction.lean
theorem isClosedMap_smul₀ {E : Type*} [Zero E] [MulActionWithZero G₀ E] [TopologicalSpace E]
    [T1Space E] [ContinuousConstSMul G₀ E] (c : G₀) : IsClosedMap fun x : E => c • x

Proof state:
case inl
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
⊢ IsClosedMap fun x => 0

Tactic:
exact isClosedMap_const

Result:
no goals

Proof state:
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
c : G₀
⊢ IsClosedMap fun x => c • x

Tactic:
rcases eq_or_ne c 0 with (rfl | hne)

Result:
case inl
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
⊢ IsClosedMap fun x => 0 • x

case inr
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
c : G₀
hne : c ≠ 0
⊢ IsClosedMap fun x => c • x

Proof state:
case inr
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
c : G₀
hne : c ≠ 0
⊢ IsClosedMap fun x => c • x

Tactic:
exact (Homeomorph.smulOfNeZero c hne).isClosedMap

Result:
no goals

Proof state:
case inl
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
⊢ IsClosedMap fun x => 0 • x

Tactic:
simp only [zero_smul]

Result:
case inl
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
⊢ IsClosedMap fun x => 0
-- Mathlib/CategoryTheory/Sites/Subsheaf.lean
theorem Sheaf.toImage_ι {F F' : Sheaf J (Type w)} (f : F ⟶ F') :
    toImage f ≫ imageι f = f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ toImage f ≫ imageι f = f

Tactic:
ext1

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ (toImage f ≫ imageι f).val = f.val

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ (toImage f ≫ imageι f).val = f.val

Tactic:
simp [Subpresheaf.toRangeSheafify]

Result:
no goals
-- Mathlib/Data/Fintype/BigOperators.lean
lemma card_filter_piFinset_const (s : Finset κ) (i : ι) (j : κ) :
    #{f ∈ piFinset fun _ ↦ s | f i = j} = if j ∈ s then #s ^ (card ι - 1) else 0 :=
  (card_filter_piFinset_eq _ _ _).trans <| by
    rw [prod_const #s, card_erase_of_mem (mem_univ _), card_univ]

Proof state:
ι : Type u_4
κ : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : Fintype ι
s : Finset κ
i : ι
j : κ
⊢ (if j ∈ s then ∏ b ∈ univ.erase i, #s else 0) = if j ∈ s then #s ^ (card ι - 1) else 0

Tactic:
rw [prod_const #s, card_erase_of_mem (mem_univ _), card_univ]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem all (f) : ∀ {s}, ValidFor l m r s → s.all f = m.all f
  | _, h => by simp [Substring.all, h.any, List.all_eq_not_any_not]

Proof state:
l m r : List Char
f : Char → Bool
x✝ : Substring
h : ValidFor l m r x✝
⊢ x✝.all f = m.all f

Tactic:
simp [Substring.all, h.any, List.all_eq_not_any_not]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Basis.lean
@[simp] lemma basisOf_vadd (v : V) (b : AffineBasis ι k P) : (v +ᵥ b).basisOf = b.basisOf

Proof state:
case h.a
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
v : V
b : AffineBasis ι k P
x✝ : ι
i✝ : { j // j ≠ x✝ }
⊢ ((v +ᵥ b).basisOf x✝) i✝ = (b.basisOf x✝) i✝

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
v : V
b : AffineBasis ι k P
⊢ (v +ᵥ b).basisOf = b.basisOf

Tactic:
ext

Result:
case h.a
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
v : V
b : AffineBasis ι k P
x✝ : ι
i✝ : { j // j ≠ x✝ }
⊢ ((v +ᵥ b).basisOf x✝) i✝ = (b.basisOf x✝) i✝
-- Mathlib/Topology/CWComplex/Classical/Basic.lean
lemma CWComplex.mapsTo [CWComplex C] (n : ℕ) (i : cell C n) : ∃ I : Π m, Finset (cell C m),
    MapsTo (map n i) (sphere 0 1) (⋃ (m < n) (j ∈ I m), map m j '' closedBall 0 1)

Proof state:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
i : cell C n
this : ∃ I, MapsTo (↑(map n i)) (sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)
⊢ ∃ I, MapsTo (↑(map n i)) (sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)

Tactic:
exact this

Result:
no goals

Proof state:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
i : cell C n
this : ∃ I, MapsTo (↑(map n i)) (sphere 0 1) (∅ ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)
⊢ ∃ I, MapsTo (↑(map n i)) (sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)

Tactic:
simp_rw [empty_union] at this

Result:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
i : cell C n
this : ∃ I, MapsTo (↑(map n i)) (sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)
⊢ ∃ I, MapsTo (↑(map n i)) (sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)

Proof state:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
i : cell C n
⊢ ∃ I, MapsTo (↑(map n i)) (sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)

Tactic:
have := RelCWComplex.mapsTo n i

Result:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
i : cell C n
this : ∃ I, MapsTo (↑(map n i)) (sphere 0 1) (∅ ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)
⊢ ∃ I, MapsTo (↑(map n i)) (sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)
-- Mathlib/Combinatorics/SimpleGraph/Prod.lean
theorem Connected.boxProd (hG : G.Connected) (hH : H.Connected) : (G □ H).Connected

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Connected
hH : H.Connected
this : Nonempty α
⊢ (G □ H).Connected

Tactic:
haveI := hH.nonempty

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Connected
hH : H.Connected
this✝ : Nonempty α
this : Nonempty β
⊢ (G □ H).Connected

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Connected
hH : H.Connected
this✝ : Nonempty α
this : Nonempty β
⊢ (G □ H).Connected

Tactic:
exact ⟨hG.preconnected.boxProd hH.preconnected⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Connected
hH : H.Connected
⊢ (G □ H).Connected

Tactic:
haveI := hG.nonempty

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
hG : G.Connected
hH : H.Connected
this : Nonempty α
⊢ (G □ H).Connected
-- Mathlib/RingTheory/Localization/InvSubmonoid.lean
theorem span_invSubmonoid : Submodule.span R (invSubmonoid M S : Set S) = ⊤

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
⊢ x ∈ Submodule.span R ↑(invSubmonoid M S)

Tactic:
rcases IsLocalization.surj'' M x with ⟨r, m, rfl⟩

Result:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
r : R
m : ↥M
⊢ r • ↑((toInvSubmonoid M S) m) ∈ Submodule.span R ↑(invSubmonoid M S)

Proof state:
case intro.intro
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
r : R
m : ↥M
⊢ r • ↑((toInvSubmonoid M S) m) ∈ Submodule.span R ↑(invSubmonoid M S)

Tactic:
exact Submodule.smul_mem _ _ (Submodule.subset_span (toInvSubmonoid M S m).prop)

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
⊢ ⊤ ≤ Submodule.span R ↑(invSubmonoid M S)

Tactic:
rintro x -

Result:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
⊢ x ∈ Submodule.span R ↑(invSubmonoid M S)

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
⊢ Submodule.span R ↑(invSubmonoid M S) = ⊤

Tactic:
rw [eq_top_iff]

Result:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
⊢ ⊤ ≤ Submodule.span R ↑(invSubmonoid M S)
-- Mathlib/Data/Matrix/Reflection.lean
theorem etaExpand_eq {m n} (A : Matrix (Fin m) (Fin n) α) : etaExpand A = A

Proof state:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin n) α
⊢ ((Equiv.refl (Fin m → Fin n → α)) fun i j => A i j) = A

Tactic:
erw [Equiv.refl_apply]

Result:
no goals

Proof state:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin n) α
⊢ A.etaExpand = A

Tactic:
simp_rw [etaExpand, FinVec.etaExpand_eq, Matrix.of]

Result:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin n) α
⊢ ((Equiv.refl (Fin m → Fin n → α)) fun i j => A i j) = A
-- Mathlib/Topology/Inseparable.lean
lemma SpecializingMap.comp {f : X → Y} {g : Y → Z}
    (hf : SpecializingMap f) (hg : SpecializingMap g) :
    SpecializingMap (g ∘ f)

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : ∀ (s : Set X), StableUnderSpecialization s → StableUnderSpecialization (f '' s)
hg : ∀ (s : Set Y), StableUnderSpecialization s → StableUnderSpecialization (g '' s)
⊢ ∀ (s : Set X), StableUnderSpecialization s → StableUnderSpecialization (g '' (f '' s))

Tactic:
exact fun s h ↦ hg _ (hf  _ h)

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : SpecializingMap f
hg : SpecializingMap g
⊢ SpecializingMap (g ∘ f)

Tactic:
simp only [specializingMap_iff_stableUnderSpecialization_image, Set.image_comp] at *

Result:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : ∀ (s : Set X), StableUnderSpecialization s → StableUnderSpecialization (f '' s)
hg : ∀ (s : Set Y), StableUnderSpecialization s → StableUnderSpecialization (g '' s)
⊢ ∀ (s : Set X), StableUnderSpecialization s → StableUnderSpecialization (g '' (f '' s))
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem strictAntiOn_log : StrictAntiOn log (Set.Iio 0)

Proof state:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ |y| < |x|

Tactic:
rwa [abs_of_neg hy, abs_of_neg hx, neg_lt_neg_iff]

Result:
no goals

Proof state:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ log |y| < log |x|

Tactic:
refine log_lt_log (abs_pos.2 hy.ne) ?_

Result:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ |y| < |x|

Proof state:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ log y < log x

Tactic:
rw [← log_abs y, ← log_abs x]

Result:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ log |y| < log |x|

Proof state:
⊢ StrictAntiOn log (Iio 0)

Tactic:
rintro x (hx : x < 0) y (hy : y < 0) hxy

Result:
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ log y < log x
-- Mathlib/Data/Finsupp/MonomialOrder.lean
lemma le_add_right (a b : σ →₀ ℕ) :
    m.toSyn a ≤ m.toSyn a + m.toSyn b

Proof state:
σ : Type u_1
m : MonomialOrder σ
a b : σ →₀ ℕ
⊢ m.toSyn a ≤ m.toSyn a + m.toSyn b

Tactic:
rw [← map_add]

Result:
σ : Type u_1
m : MonomialOrder σ
a b : σ →₀ ℕ
⊢ m.toSyn a ≤ m.toSyn (a + b)

Proof state:
σ : Type u_1
m : MonomialOrder σ
a b : σ →₀ ℕ
⊢ m.toSyn a ≤ m.toSyn (a + b)

Tactic:
exact m.toSyn_monotone le_self_add

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem infsep_pair_eq_toReal : ({x, y} : Set α).infsep = (edist x y).toReal

Proof state:
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hxy : x = y
⊢ {y, y}.infsep = (edist y y).toReal

Tactic:
simp only [infsep_singleton, pair_eq_singleton, edist_self, ENNReal.zero_toReal]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
⊢ {x, y}.infsep = (edist x y).toReal

Tactic:
by_cases hxy : x = y

Result:
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hxy : x = y
⊢ {x, y}.infsep = (edist x y).toReal

case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hxy : ¬x = y
⊢ {x, y}.infsep = (edist x y).toReal

Proof state:
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hxy : x = y
⊢ {x, y}.infsep = (edist x y).toReal

Tactic:
rw [hxy]

Result:
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hxy : x = y
⊢ {y, y}.infsep = (edist y y).toReal

Proof state:
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hxy : ¬x = y
⊢ {x, y}.infsep = (edist x y).toReal

Tactic:
rw [infsep, einfsep_pair hxy]

Result:
no goals