harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Trace.lean
theorem trace_tensorProduct' (f : M →ₗ[R] M) (g : N →ₗ[R] N) :
    trace R (M ⊗ N) (map f g) = trace R M f * trace R N g

Proof state:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
h : (((mapBilinear R M N M N).compr₂ (trace R (M ⊗[R] N))) f) g = (((lsmul R R).compl₁₂ (trace R M) (trace R N)) f) g
⊢ (trace R (M ⊗[R] N)) (map f g) = (trace R M) f * (trace R N) g

Tactic:
simp only [compr₂_apply, mapBilinear_apply, compl₁₂_apply, lsmul_apply,
  Algebra.id.smul_eq_mul] at h

Result:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
h : (trace R (M ⊗[R] N)) (map f g) = (trace R M) f * (trace R N) g
⊢ (trace R (M ⊗[R] N)) (map f g) = (trace R M) f * (trace R N) g

Proof state:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
h : (trace R (M ⊗[R] N)) (map f g) = (trace R M) f * (trace R N) g
⊢ (trace R (M ⊗[R] N)) (map f g) = (trace R M) f * (trace R N) g

Tactic:
exact h

Result:
no goals

Proof state:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
⊢ (trace R (M ⊗[R] N)) (map f g) = (trace R M) f * (trace R N) g

Tactic:
have h := LinearMap.ext_iff.1 (LinearMap.ext_iff.1 (trace_tensorProduct R M N) f) g

Result:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
h : (((mapBilinear R M N M N).compr₂ (trace R (M ⊗[R] N))) f) g = (((lsmul R R).compl₁₂ (trace R M) (trace R N)) f) g
⊢ (trace R (M ⊗[R] N)) (map f g) = (trace R M) f * (trace R N) g
-- Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean
theorem MemLp.sub {f g : α → E} (hf : MemLp f p μ) (hg : MemLp g p μ) : MemLp (f - g) p μ

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ MemLp (f - g) p μ

Tactic:
rw [sub_eq_add_neg]

Result:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ MemLp (f + -g) p μ

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ MemLp (f + -g) p μ

Tactic:
exact hf.add hg.neg

Result:
no goals
-- Mathlib/SetTheory/Ordinal/CantorNormalForm.lean
theorem CNF_lt_snd {b o : Ordinal.{u}} {x : Ordinal × Ordinal} : x ∈ CNF b o → 0 < x.2

Proof state:
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b 0 → 0 < x.2

Tactic:
simp

Result:
no goals

Proof state:
case head
b o✝ o : Ordinal.{u}
ho : o ≠ 0
IH : (log b o, o / b ^ log b o) ∈ CNF b (o % b ^ log b o) → 0 < (log b o, o / b ^ log b o).2
⊢ 0 < (log b o, o / b ^ log b o).2

Tactic:
exact div_opow_log_pos b ho

Result:
no goals

Proof state:
case tail
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.2
h : Mem x (CNF b (o % b ^ log b o))
⊢ 0 < x.2

Tactic:
exact IH h

Result:
no goals

Proof state:
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.2
⊢ x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) → 0 < x.2

Tactic:
rintro (h | ⟨_, h⟩)

Result:
case head
b o✝ o : Ordinal.{u}
ho : o ≠ 0
IH : (log b o, o / b ^ log b o) ∈ CNF b (o % b ^ log b o) → 0 < (log b o, o / b ^ log b o).2
⊢ 0 < (log b o, o / b ^ log b o).2

case tail
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.2
h : Mem x (CNF b (o % b ^ log b o))
⊢ 0 < x.2

Proof state:
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.2
⊢ x ∈ CNF b o → 0 < x.2

Tactic:
rw [CNF_ne_zero ho]

Result:
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.2
⊢ x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) → 0 < x.2

Proof state:
b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b o → 0 < x.2

Tactic:
refine CNFRec b (by simp) (fun o ho IH ↦ ?_) o

Result:
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.2
⊢ x ∈ CNF b o → 0 < x.2
-- Mathlib/RingTheory/Noetherian/Nilpotent.lean
theorem IsNoetherianRing.isNilpotent_nilradical (R : Type*) [CommSemiring R] [IsNoetherianRing R] :
    IsNilpotent (nilradical R)

Proof state:
case intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsNoetherianRing R
n : ℕ
hn : ⊥.radical ^ n ≤ ⊥
⊢ IsNilpotent (nilradical R)

Tactic:
exact ⟨n, eq_bot_iff.mpr hn⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsNoetherianRing R
⊢ IsNilpotent (nilradical R)

Tactic:
obtain ⟨n, hn⟩ := Ideal.exists_radical_pow_le_of_fg (⊥ : Ideal R) (IsNoetherian.noetherian _)

Result:
case intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsNoetherianRing R
n : ℕ
hn : ⊥.radical ^ n ≤ ⊥
⊢ IsNilpotent (nilradical R)
-- Mathlib/MeasureTheory/Function/EssSup.lean
theorem essSup_comp_le_essSup_map_measure (hf : AEMeasurable f μ) :
    essSup (g ∘ f) μ ≤ essSup g (Measure.map f μ)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f μ
⊢ map g (map f (ae μ)) ≤ map g (ae (Measure.map f μ))

Tactic:
exact Filter.map_mono (Measure.tendsto_ae_map hf)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f μ
⊢ map (g ∘ f) (ae μ) ≤ map g (ae (Measure.map f μ))

Tactic:
rw [← Filter.map_map]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f μ
⊢ map g (map f (ae μ)) ≤ map g (ae (Measure.map f μ))

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f μ
⊢ essSup (g ∘ f) μ ≤ essSup g (Measure.map f μ)

Tactic:
refine limsSup_le_limsSup_of_le ?_

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLattice β
γ : Type u_3
mγ : MeasurableSpace γ
f : α → γ
g : γ → β
hf : AEMeasurable f μ
⊢ map (g ∘ f) (ae μ) ≤ map g (ae (Measure.map f μ))
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem range_image_pred_top_sub (n : ℕ) :
    ((Finset.range n).image fun j => n - 1 - j) = Finset.range n

Proof state:
case zero

⊢ image (fun j => 0 - 1 - j) (range 0) = range 0

Tactic:
rw [range_zero, image_empty]

Result:
no goals

Proof state:
n : ℕ
⊢ image (fun j => n - 1 - j) (range n) = range n

Tactic:
cases n

Result:
case zero

⊢ image (fun j => 0 - 1 - j) (range 0) = range 0

case succ
n✝ : ℕ
⊢ image (fun j => n✝ + 1 - 1 - j) (range (n✝ + 1)) = range (n✝ + 1)

Proof state:
case succ
n✝ : ℕ
⊢ image (fun j => n✝ + 1 - 1 - j) (range (n✝ + 1)) = range (n✝ + 1)

Tactic:
rw [Finset.range_eq_Ico, Nat.Ico_image_const_sub_eq_Ico (Nat.zero_le _)]

Result:
case succ
n✝ : ℕ
⊢ Ico (n✝ + 1 - 1 + 1 - (n✝ + 1)) (n✝ + 1 - 1 + 1 - 0) = Ico 0 (n✝ + 1)

Proof state:
case succ
n✝ : ℕ
⊢ Ico (n✝ + 1 - 1 + 1 - (n✝ + 1)) (n✝ + 1 - 1 + 1 - 0) = Ico 0 (n✝ + 1)

Tactic:
simp_rw [succ_sub_succ, Nat.sub_zero, Nat.sub_self]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem degree_map_eq_of_injective (hf : Injective f) (p : R[X]) : degree (p.map f) = degree p :=
  letI := Classical.decEq R
  if h : p = 0 then by simp [h]
  else
    degree_map_eq_of_leadingCoeff_ne_zero _
      (by rw [← f.map_zero]; exact mt hf.eq_iff.1 (mt leadingCoeff_eq_zero.1 h))

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ⇑f
p : R[X]
this : DecidableEq R := Classical.decEq R
h : p = 0
⊢ (map f p).degree = p.degree

Tactic:
simp [h]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ⇑f
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬p = 0
⊢ f p.leadingCoeff ≠ f 0

Tactic:
exact mt hf.eq_iff.1 (mt leadingCoeff_eq_zero.1 h)

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ⇑f
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬p = 0
⊢ f p.leadingCoeff ≠ 0

Tactic:
rw [← f.map_zero]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ⇑f
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬p = 0
⊢ f p.leadingCoeff ≠ f 0
-- Mathlib/FieldTheory/Finite/Polynomial.lean
theorem eval_indicator_apply_eq_zero (a b : σ → K) (h : a ≠ b) : eval a (indicator b) = 0

Proof state:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
⊢ ∃ i, a i ≠ b i

Tactic:
rwa [Ne, funext_iff, not_forall] at h

Result:
no goals

Proof state:
case intro
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ ∃ a_1 ∈ Finset.univ, 1 - (a a_1 - b a_1) ^ (Fintype.card K - 1) = 0

Tactic:
refine ⟨i, Finset.mem_univ _, ?_⟩

Result:
case intro
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ 1 - (a i - b i) ^ (Fintype.card K - 1) = 0

Proof state:
case intro
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ 1 - (a i - b i) ^ (Fintype.card K - 1) = 0

Tactic:
rw [FiniteField.pow_card_sub_one_eq_one, sub_self]

Result:
case intro.ha
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ a i - b i ≠ 0

Proof state:
case intro
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ (eval a) (indicator b) = 0

Tactic:
simp only [indicator, map_prod, map_sub, map_one, map_pow, eval_X, eval_C, sub_self,
  Finset.prod_eq_zero_iff]

Result:
case intro
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ ∃ a_1 ∈ Finset.univ, 1 - (a a_1 - b a_1) ^ (Fintype.card K - 1) = 0

Proof state:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
⊢ (eval a) (indicator b) = 0

Tactic:
obtain ⟨i, hi⟩ : ∃ i, a i ≠ b i := by rwa [Ne, funext_iff, not_forall] at h

Result:
case intro
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ (eval a) (indicator b) = 0

Proof state:
case intro.ha
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : Field K
a b : σ → K
h : a ≠ b
i : σ
hi : a i ≠ b i
⊢ a i - b i ≠ 0

Tactic:
rwa [Ne, sub_eq_zero]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem CliqueFree.sup_edge (h : G.CliqueFree n) (v w : α) :
    (G ⊔ edge v w).CliqueFree (n + 1)

Proof state:
case map_rel_iff'
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
x : Fin (n + 1)
hx : f x = w
a b : Fin n
⊢ G.Adj (f (x.succAbove a)) (f (x.succAbove b)) ↔ a ≠ b

Tactic:
have hs := @ha (x.succAbove a) (x.succAbove b)

Result:
case map_rel_iff'
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
x : Fin (n + 1)
hx : f x = w
a b : Fin n
hs : (G ⊔ edge v w).Adj (f (x.succAbove a)) (f (x.succAbove b)) ↔ ¬x.succAbove a = x.succAbove b
⊢ G.Adj (f (x.succAbove a)) (f (x.succAbove b)) ↔ a ≠ b

Proof state:
case map_rel_iff'
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
mw : w ∉ Set.range ⇑f
a b : Fin n
⊢ G.Adj (f a.succ) (f b.succ) ↔ a ≠ b

Tactic:
have hs := @ha a.succ b.succ

Result:
case map_rel_iff'
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
mw : w ∉ Set.range ⇑f
a b : Fin n
hs : (G ⊔ edge v w).Adj (f a.succ) (f b.succ) ↔ ¬a.succ = b.succ
⊢ G.Adj (f a.succ) (f b.succ) ↔ a ≠ b

Proof state:
case map_rel_iff'
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
mw : w ∉ Set.range ⇑f
a b : Fin n
hs : (G ⊔ edge v w).Adj (f a.succ) (f b.succ) ↔ ¬a.succ = b.succ
ia : f a.succ ≠ w
ib : f b.succ ≠ w
⊢ G.Adj (f a.succ) (f b.succ) ↔ a ≠ b

Tactic:
rw [sup_adj, edge_adj] at hs

Result:
case map_rel_iff'
α : Type u_1
G : SimpleGraph α
n : ℕ
v w : α
h : ¬(G ⊔ edge v w).CliqueFree (n + 1)
f : Fin (n + 1) ↪ α
ha : ∀ {a b : Fin (n + 1)}, (G ⊔ edge v w).Adj (f a) (f b) ↔ ¬a = b
mw : w ∉ Set.range ⇑f
a b : Fin n
hs :
  G.Adj (f a.succ) (f b.succ) ∨ (f a.succ = v ∧ f b.succ = w ∨ f a.succ = w ∧ f b.succ = v) ∧ f a.succ ≠ f b.succ ↔
    ¬a.succ = b.succ
ia : f a.succ ≠ w
ib : f b.succ ≠ w
⊢ G.Adj (f a.succ) (f b.succ) ↔ a ≠ b
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mpullback_add :
    mpullback I I' f (V + V₁) = mpullback I I' f V + mpullback I I' f V₁

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
V V₁ : (x : M') → TangentSpace I' x
⊢ mpullback I I' f (V + V₁) = mpullback I I' f V + mpullback I I' f V₁

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
V V₁ : (x : M') → TangentSpace I' x
x : M
⊢ mpullback I I' f (V + V₁) x = (mpullback I I' f V + mpullback I I' f V₁) x

Proof state:
case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
V V₁ : (x : M') → TangentSpace I' x
x : M
⊢ mpullback I I' f (V + V₁) x = (mpullback I I' f V + mpullback I I' f V₁) x

Tactic:
simp [mpullback_apply]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem zero_of_source_iso_zero {X Y : C} (f : X ⟶ Y) (i : X ≅ 0) : f = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : X ≅ 0
⊢ f = 0

Tactic:
have h : f = i.hom ≫ 𝟙 0 ≫ i.inv ≫ f := by simp only [Iso.hom_inv_id_assoc, id_comp, comp_id]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : X ≅ 0
h : f = i.hom ≫ 𝟙 0 ≫ i.inv ≫ f
⊢ f = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : X ≅ 0
h : f = i.hom ≫ 𝟙 0 ≫ i.inv ≫ f
⊢ f = 0

Tactic:
simpa using h

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : X ≅ 0
⊢ f = i.hom ≫ 𝟙 0 ≫ i.inv ≫ f

Tactic:
simp only [Iso.hom_inv_id_assoc, id_comp, comp_id]

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem isSimpleOrder_iff [BoundedOrder α] [BoundedOrder β] (f : α ≃o β) :
    IsSimpleOrder α ↔ IsSimpleOrder β

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
f : α ≃o β
⊢ IsSimpleOrder α ↔ IsSimpleOrder β

Tactic:
rw [isSimpleOrder_iff_isAtom_top, isSimpleOrder_iff_isAtom_top, ← f.isAtom_iff ⊤,
  f.map_top]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem DistinctKeys.insertEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α}
    {v : β k} (h : DistinctKeys l) : DistinctKeys (insertEntry k v l)

Proof state:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
v : β k
h : DistinctKeys l
h' : containsKey k l = false
⊢ DistinctKeys l ∧ containsKey k l = false

Tactic:
exact ⟨h, h'⟩

Result:
no goals

Proof state:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
v : β k
h : DistinctKeys l
h' : containsKey k l = true
⊢ DistinctKeys (List.insertEntry k v l)

Tactic:
rw [insertEntry_of_containsKey h']

Result:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
v : β k
h : DistinctKeys l
h' : containsKey k l = true
⊢ DistinctKeys (List.replaceEntry k v l)

Proof state:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
v : β k
h : DistinctKeys l
h' : containsKey k l = true
⊢ DistinctKeys (List.replaceEntry k v l)

Tactic:
exact h.replaceEntry

Result:
no goals

Proof state:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
v : β k
h : DistinctKeys l
h' : containsKey k l = false
⊢ DistinctKeys (List.insertEntry k v l)

Tactic:
rw [insertEntry_of_containsKey_eq_false h', distinctKeys_cons_iff]

Result:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
v : β k
h : DistinctKeys l
h' : containsKey k l = false
⊢ DistinctKeys l ∧ containsKey k l = false

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
v : β k
h : DistinctKeys l
⊢ DistinctKeys (List.insertEntry k v l)

Tactic:
cases h' : containsKey k l

Result:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
v : β k
h : DistinctKeys l
h' : containsKey k l = false
⊢ DistinctKeys (List.insertEntry k v l)

case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
v : β k
h : DistinctKeys l
h' : containsKey k l = true
⊢ DistinctKeys (List.insertEntry k v l)
-- Mathlib/CategoryTheory/Sites/OneHypercover.lean
lemma sieve₁'_eq_sieve₁ : E.sieve₁' i₁ i₂ = E.sieve₁ (pullback.fst _ _) (pullback.snd _ _)

Proof state:
case e_h
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
⊢ 𝟙 (pullback (E.f i₁) (E.f i₂)) = pullback.lift (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂)) ⋯

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
⊢ Sieve.pullback (𝟙 (pullback (E.f i₁) (E.f i₂))) (E.sieve₁' i₁ i₂) =
    Sieve.pullback (pullback.lift (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂)) ⋯) (E.sieve₁' i₁ i₂)

Tactic:
congr

Result:
case e_h
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
⊢ 𝟙 (pullback (E.f i₁) (E.f i₂)) = pullback.lift (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂)) ⋯

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
⊢ E.sieve₁' i₁ i₂ = E.sieve₁ (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂))

Tactic:
rw [← Sieve.pullback_id (S := E.sieve₁' i₁ i₂),
  sieve₁_eq_pullback_sieve₁' _ _ _ pullback.condition]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
⊢ Sieve.pullback (𝟙 (pullback (E.f i₁) (E.f i₂))) (E.sieve₁' i₁ i₂) =
    Sieve.pullback (pullback.lift (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂)) ⋯) (E.sieve₁' i₁ i₂)
-- Mathlib/Algebra/DirectSum/Internal.lean
theorem SetLike.algebraMap_mem_graded [Zero ι] [CommSemiring S] [Semiring R] [Algebra S R]
    (A : ι → Submodule S R) [SetLike.GradedOne A] (s : S) : algebraMap S R s ∈ A 0

Proof state:
ι : Type u_1
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : CommSemiring S
inst✝² : Semiring R
inst✝¹ : Algebra S R
A : ι → Submodule S R
inst✝ : GradedOne A
s : S
⊢ s • 1 ∈ A 0

Tactic:
exact (A 0).smul_mem s <| SetLike.one_mem_graded _

Result:
no goals

Proof state:
ι : Type u_1
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : CommSemiring S
inst✝² : Semiring R
inst✝¹ : Algebra S R
A : ι → Submodule S R
inst✝ : GradedOne A
s : S
⊢ (algebraMap S R) s ∈ A 0

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Result:
ι : Type u_1
S : Type u_3
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : CommSemiring S
inst✝² : Semiring R
inst✝¹ : Algebra S R
A : ι → Submodule S R
inst✝ : GradedOne A
s : S
⊢ s • 1 ∈ A 0
-- Mathlib/Topology/Homotopy/Basic.lean
theorem symm_symm {f₀ f₁ : C(X, Y)} (F : Homotopy f₀ f₁) : F.symm.symm = F

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
⊢ F.symm.symm = F

Tactic:
ext

Result:
case h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
x✝ : ↑I × X
⊢ F.symm.symm x✝ = F x✝

Proof state:
case h
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ : C(X, Y)
F : f₀.Homotopy f₁
x✝ : ↑I × X
⊢ F.symm.symm x✝ = F x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem card_edgeFinset_le_card_choose_two : #G.edgeFinset ≤ (Fintype.card V).choose 2

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
⊢ #G.edgeFinset ≤ (Fintype.card V).choose 2

Tactic:
classical
rw [← card_edgeFinset_top_eq_card_choose_two]
exact card_le_card (edgeFinset_mono le_top)

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
⊢ #G.edgeFinset ≤ (Fintype.card V).choose 2

Tactic:
rw [← card_edgeFinset_top_eq_card_choose_two]

Result:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
⊢ #G.edgeFinset ≤ #⊤.edgeFinset

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
⊢ #G.edgeFinset ≤ #⊤.edgeFinset

Tactic:
exact card_le_card (edgeFinset_mono le_top)

Result:
no goals