harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/Block.lean
theorem BlockTriangular.det_fintype [DecidableEq α] [Fintype α] [LinearOrder α]
    (h : BlockTriangular M b) : M.det = ∏ k : α, (M.toSquareBlock b k).det

Proof state:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
h : M.BlockTriangular b
⊢ M.det = ∏ k : α, (M.toSquareBlock b k).det

Tactic:
refine h.det.trans (prod_subset (subset_univ _) fun a _ ha => ?_)

Result:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
h : M.BlockTriangular b
a : α
x✝ : a ∈ univ
ha : a ∉ image b univ
⊢ (M.toSquareBlock b a).det = 1

Proof state:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
h : M.BlockTriangular b
a : α
x✝ : a ∈ univ
ha : a ∉ image b univ
⊢ (M.toSquareBlock b a).det = 1

Tactic:
have : IsEmpty { i // b i = a } := ⟨fun i => ha <| mem_image.2 ⟨i, mem_univ _, i.2⟩⟩

Result:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
h : M.BlockTriangular b
a : α
x✝ : a ∈ univ
ha : a ∉ image b univ
this : IsEmpty { i // b i = a }
⊢ (M.toSquareBlock b a).det = 1

Proof state:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
h : M.BlockTriangular b
a : α
x✝ : a ∈ univ
ha : a ∉ image b univ
this : IsEmpty { i // b i = a }
⊢ (M.toSquareBlock b a).det = 1

Tactic:
exact det_isEmpty

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem finSigmaFinEquiv_one {n : Fin 1 → ℕ} (ij : (i : Fin 1) × Fin (n i)) :
    (finSigmaFinEquiv ij : ℕ) = ij.2

Proof state:
n : Fin 1 → ℕ
ij : (i : Fin 1) × Fin (n i)
⊢ ∑ i : Fin ↑ij.fst, n (Fin.castLE ⋯ i) = 0

Tactic:
apply @Finset.sum_of_isEmpty _ _ _ _ (by simpa using Fin.isEmpty')

Result:
no goals

Proof state:
n : Fin 1 → ℕ
ij : (i : Fin 1) × Fin (n i)
⊢ ↑(finSigmaFinEquiv ij) = ↑ij.snd

Tactic:
rw [finSigmaFinEquiv_apply, add_left_eq_self]

Result:
n : Fin 1 → ℕ
ij : (i : Fin 1) × Fin (n i)
⊢ ∑ i : Fin ↑ij.fst, n (Fin.castLE ⋯ i) = 0

Proof state:
n : Fin 1 → ℕ
ij : (i : Fin 1) × Fin (n i)
⊢ IsEmpty (Fin ↑ij.fst)

Tactic:
simpa using Fin.isEmpty'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Relabel.lean
theorem relabel_size_eq_size {aig : AIG α} {r : α → β} :
    (aig.relabel r).decls.size = aig.decls.size

Proof state:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
r : α → β
⊢ (relabel r aig).decls.size = aig.decls.size

Tactic:
simp [relabel]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Composition.lean
lemma comp [L₁.IsLocalization W₁] [L₂.IsLocalization W₂]
    (W₃ : MorphismProperty C₁) (hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂))
    (hW₁₃ : W₁ ≤ W₃) (hW₂₃ : W₂ ≤ W₃.map L₁) :
    (L₁ ⋙ L₂).IsLocalization W₃

Proof state:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
L₁ : C₁ ⥤ C₂
L₂ : C₂ ⥤ C₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝¹ : L₁.IsLocalization W₁
inst✝ : L₂.IsLocalization W₂
W₃ : MorphismProperty C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
⊢ (L₁ ⋙ L₂).IsLocalization W₃

Tactic:
let Φ : LocalizerMorphism W₂ W₂' :=
  { functor := E₂.functor
    map := by
      have eq := W₂.isoClosure.inverseImage_map_eq_of_isEquivalence E₂.functor
      rw [MorphismProperty.map_isoClosure] at eq
      rw [eq]
      apply W₂.le_isoClosure }

Result:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
L₁ : C₁ ⥤ C₂
L₂ : C₂ ⥤ C₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝¹ : L₁.IsLocalization W₁
inst✝ : L₂.IsLocalization W₂
W₃ : MorphismProperty C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := { functor := E₂.functor, map := ⋯ }
⊢ (L₁ ⋙ L₂).IsLocalization W₃
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
@[simp] lemma prob_compl_eq_one_iff₀ (hs : NullMeasurableSet s μ) : μ sᶜ = 1 ↔ μ s = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsProbabilityMeasure μ
hs : NullMeasurableSet s μ
⊢ μ sᶜ = 1 ↔ μ s = 0

Tactic:
rw [← prob_compl_eq_zero_iff₀ hs.compl, compl_compl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem val_add_one {n : Nat} (i : Fin (n + 1)) :
    ((i + 1 : Fin (n + 1)) : Nat) = if i = last _ then (0 : Nat) else i + 1

Proof state:
case refl
n : Nat
h : ↑(last n) = ↑(last n)
⊢ ↑(last n + 1) = if last n = last n then 0 else ↑(last n) + 1

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
i : Fin (n + 1)
⊢ ↑(i + 1) = if i = last n then 0 else ↑i + 1

Tactic:
match Nat.eq_or_lt_of_le (le_last i) with
| .inl h => cases Fin.eq_of_val_eq h; simp
| .inr h => simpa [Fin.ne_of_lt h] using val_add_one_of_lt h

Result:
no goals

Proof state:
n : Nat
i : Fin (n + 1)
h : ↑i < ↑(last n)
⊢ ↑(i + 1) = if i = last n then 0 else ↑i + 1

Tactic:
simpa [Fin.ne_of_lt h] using val_add_one_of_lt h

Result:
no goals

Proof state:
n : Nat
i : Fin (n + 1)
h : ↑i = ↑(last n)
⊢ ↑(i + 1) = if i = last n then 0 else ↑i + 1

Tactic:
cases Fin.eq_of_val_eq h

Result:
case refl
n : Nat
h : ↑(last n) = ↑(last n)
⊢ ↑(last n + 1) = if last n = last n then 0 else ↑(last n) + 1
-- Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
lemma growsPolynomially_id : GrowsPolynomially (fun x => x)

Proof state:
case h
b : ℝ
hb : b ∈ Set.Ioo 0 1
x u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ b * x ≤ u ∧ u ≤ x

Tactic:
exact ⟨hu.1, hu.2⟩

Result:
no goals

Proof state:
b : ℝ
hb : b ∈ Set.Ioo 0 1
⊢ ∃ c₂ > 0,
    ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => x) u ∈ Set.Icc (b * (fun x => x) x) (c₂ * (fun x => x) x)

Tactic:
refine ⟨1, by norm_num, ?_⟩

Result:
b : ℝ
hb : b ∈ Set.Ioo 0 1
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => x) u ∈ Set.Icc (b * (fun x => x) x) (1 * (fun x => x) x)

Proof state:
case h
b : ℝ
hb : b ∈ Set.Ioo 0 1
x u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ u ∈ Set.Icc (b * x) (1 * x)

Tactic:
simp only [one_mul, gt_iff_lt, not_le, Set.mem_Icc]

Result:
case h
b : ℝ
hb : b ∈ Set.Ioo 0 1
x u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ b * x ≤ u ∧ u ≤ x

Proof state:
b : ℝ
hb : b ∈ Set.Ioo 0 1
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => x) u ∈ Set.Icc (c₁ * (fun x => x) x) (c₂ * (fun x => x) x)

Tactic:
refine ⟨b, hb.1, ?_⟩

Result:
b : ℝ
hb : b ∈ Set.Ioo 0 1
⊢ ∃ c₂ > 0,
    ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => x) u ∈ Set.Icc (b * (fun x => x) x) (c₂ * (fun x => x) x)

Proof state:
b : ℝ
hb : b ∈ Set.Ioo 0 1
⊢ 1 > 0

Tactic:
norm_num

Result:
no goals

Proof state:
b : ℝ
hb : b ∈ Set.Ioo 0 1
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => x) u ∈ Set.Icc (b * (fun x => x) x) (1 * (fun x => x) x)

Tactic:
filter_upwards with x u hu

Result:
case h
b : ℝ
hb : b ∈ Set.Ioo 0 1
x u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ u ∈ Set.Icc (b * x) (1 * x)

Proof state:
⊢ GrowsPolynomially fun x => x

Tactic:
intro b hb

Result:
b : ℝ
hb : b ∈ Set.Ioo 0 1
⊢ ∃ c₁ > 0,
    ∃ c₂ > 0,
      ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => x) u ∈ Set.Icc (c₁ * (fun x => x) x) (c₂ * (fun x => x) x)
-- Mathlib/RingTheory/Presentation.lean
private lemma aux_eq_comp : Q.aux P =
    (MvPolynomial.mapAlgHom (aeval P.val)).comp (sumAlgEquiv R Q.vars P.vars).toAlgHom

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
⊢ Algebra.Presentation.aux Q P = (mapAlgHom (aeval P.val)).comp ↑(sumAlgEquiv R Q.vars P.vars)

Tactic:
ext i : 1

Result:
case hf
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
i : Q.vars ⊕ P.vars
⊢ (Algebra.Presentation.aux Q P) (X i) = ((mapAlgHom (aeval P.val)).comp ↑(sumAlgEquiv R Q.vars P.vars)) (X i)

Proof state:
case hf
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T
P : Presentation R S
i : Q.vars ⊕ P.vars
⊢ (Algebra.Presentation.aux Q P) (X i) = ((mapAlgHom (aeval P.val)).comp ↑(sumAlgEquiv R Q.vars P.vars)) (X i)

Tactic:
cases i <;> simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lt_aleph0 {c : Cardinal} : c < ℵ₀ ↔ ∃ n : ℕ, c = n :=
  ⟨fun h => by
    rcases lt_lift_iff.1 h with ⟨c, h', rfl⟩
    rcases le_mk_iff_exists_set.1 h'.1 with ⟨S, rfl⟩
    suffices S.Finite by
      lift S to Finset ℕ using this
      simp
    contrapose! h'
    haveI := Infinite.to_subtype h'
    exact ⟨Infinite.natEmbedding S⟩, fun ⟨_, e⟩ => e.symm ▸ nat_lt_aleph0 _⟩

Proof state:
case intro.intro.intro
S : Set ℕ
h' : #↑S < #ℕ
h : lift.{u_1, 0} #↑S < ℵ₀
⊢ ∃ n, lift.{u_1, 0} #↑S = ↑n

Tactic:
suffices S.Finite by
  lift S to Finset ℕ using this
  simp

Result:
case intro.intro.intro
S : Set ℕ
h' : #↑S < #ℕ
h : lift.{u_1, 0} #↑S < ℵ₀
⊢ S.Finite

Proof state:
S : Set ℕ
h' : #↑S < #ℕ
h : lift.{u_1, 0} #↑S < ℵ₀
this : S.Finite
⊢ ∃ n, lift.{u_1, 0} #↑S = ↑n

Tactic:
lift S to Finset ℕ using this

Result:
case intro
S : Finset ℕ
h' : #↑↑S < #ℕ
h : lift.{u_1, 0} #↑↑S < ℵ₀
⊢ ∃ n, lift.{u_1, 0} #↑↑S = ↑n

Proof state:
case intro
S : Finset ℕ
h' : #↑↑S < #ℕ
h : lift.{u_1, 0} #↑↑S < ℵ₀
⊢ ∃ n, lift.{u_1, 0} #↑↑S = ↑n

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.intro
S : Set ℕ
h : lift.{u_1, 0} #↑S < ℵ₀
h' : ¬S.Finite
this : Infinite ↑S
⊢ #ℕ ≤ #↑S

Tactic:
exact ⟨Infinite.natEmbedding S⟩

Result:
no goals

Proof state:
case intro.intro.intro
S : Set ℕ
h' : #↑S < #ℕ
h : lift.{u_1, 0} #↑S < ℵ₀
⊢ S.Finite

Tactic:
contrapose! h'

Result:
case intro.intro.intro
S : Set ℕ
h : lift.{u_1, 0} #↑S < ℵ₀
h' : ¬S.Finite
⊢ #ℕ ≤ #↑S

Proof state:
case intro.intro
c : Cardinal.{0}
h' : c < #ℕ
h : lift.{u_1, 0} c < ℵ₀
⊢ ∃ n, lift.{u_1, 0} c = ↑n

Tactic:
rcases le_mk_iff_exists_set.1 h'.1 with ⟨S, rfl⟩

Result:
case intro.intro.intro
S : Set ℕ
h' : #↑S < #ℕ
h : lift.{u_1, 0} #↑S < ℵ₀
⊢ ∃ n, lift.{u_1, 0} #↑S = ↑n

Proof state:
case intro.intro.intro
S : Set ℕ
h : lift.{u_1, 0} #↑S < ℵ₀
h' : ¬S.Finite
⊢ #ℕ ≤ #↑S

Tactic:
haveI := Infinite.to_subtype h'

Result:
case intro.intro.intro
S : Set ℕ
h : lift.{u_1, 0} #↑S < ℵ₀
h' : ¬S.Finite
this : Infinite ↑S
⊢ #ℕ ≤ #↑S

Proof state:
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ∃ n, c = ↑n

Tactic:
rcases lt_lift_iff.1 h with ⟨c, h', rfl⟩

Result:
case intro.intro
c : Cardinal.{0}
h' : c < #ℕ
h : lift.{u_1, 0} c < ℵ₀
⊢ ∃ n, lift.{u_1, 0} c = ↑n
-- Mathlib/Data/Nat/Set.lean
theorem range_rec {α : Type*} (x : α) (f : ℕ → α → α) :
    (Set.range fun n => Nat.rec x f n : Set α) =
      {x} ∪ Set.range fun n => Nat.rec (f 0 x) (f ∘ succ) n

Proof state:
case h.e'_3.h.e'_4.h.e'_3.h.succ
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
ihn : rec (f 0 x) (f ∘ succ) n = f n (rec x f n)
⊢ rec (f 0 x) (f ∘ succ) (n + 1) = f (n + 1) (rec x f (n + 1))

Tactic:
dsimp at ihn ⊢

Result:
case h.e'_3.h.e'_4.h.e'_3.h.succ
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
ihn : rec (f 0 x) (f ∘ succ) n = f n (rec x f n)
⊢ f (n + 1) (rec (f 0 x) (f ∘ succ) n) = f (n + 1) (f n (rec x f n))

Proof state:
case h.e'_3.h.e'_4.h.e'_3.h
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
⊢ rec (f 0 x) (f ∘ succ) n = f n (rec x f n)

Tactic:
induction n with
| zero => rfl
| succ n ihn => dsimp at ihn ⊢; rw [ihn]

Result:
no goals

Proof state:
case h.e'_3.h.e'_4.h.e'_3.h
α : Type u_2
x : α
f : ℕ → α → α
x✝ : ℕ
⊢ rec (f 0 x) (f ∘ succ) x✝ = f x✝ (rec x f x✝)

Tactic:
rename_i n

Result:
case h.e'_3.h.e'_4.h.e'_3.h
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
⊢ rec (f 0 x) (f ∘ succ) n = f n (rec x f n)

Proof state:
case h.e'_3.h.e'_4.h.e'_3.h.succ
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
ihn : rec (f 0 x) (f ∘ succ) n = f n (rec x f n)
⊢ f (n + 1) (rec (f 0 x) (f ∘ succ) n) = f (n + 1) (f n (rec x f n))

Tactic:
rw [ihn]

Result:
no goals

Proof state:
case h.e'_3.h.e'_4.h.e'_3.h
α : Type u_2
x : α
f : ℕ → α → α
x✝ : ℕ
⊢ rec (f 0 x) (f ∘ succ) x✝ = ((fun n => rec x f n) ∘ succ) x✝

Tactic:
dsimp

Result:
case h.e'_3.h.e'_4.h.e'_3.h
α : Type u_2
x : α
f : ℕ → α → α
x✝ : ℕ
⊢ rec (f 0 x) (f ∘ succ) x✝ = f x✝ (rec x f x✝)

Proof state:
case h.e'_3.h.e'_4.h.e'_3.h.zero
α : Type u_2
x : α
f : ℕ → α → α
⊢ rec (f 0 x) (f ∘ succ) 0 = f 0 (rec x f 0)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
x : α
f : ℕ → α → α
⊢ (range fun n => rec x f n) = {x} ∪ range fun n => rec (f 0 x) (f ∘ succ) n

Tactic:
convert (range_of_succ (fun n => Nat.rec x f n : ℕ → α)).symm using 4

Result:
case h.e'_3.h.e'_4.h.e'_3.h
α : Type u_2
x : α
f : ℕ → α → α
x✝ : ℕ
⊢ rec (f 0 x) (f ∘ succ) x✝ = ((fun n => rec x f n) ∘ succ) x✝
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem singleton_injective : Function.Injective (@singleton ZFSet ZFSet _) := fun x y H => by
  let this := congr_arg sUnion H
  rwa [sUnion_singleton, sUnion_singleton] at this

Proof state:
x y : ZFSet.{u_1}
H : {x} = {y}
⊢ x = y

Tactic:
let this := congr_arg sUnion H

Result:
x y : ZFSet.{u_1}
H : {x} = {y}
this : ⋃₀ {x} = ⋃₀ {y} := congr_arg sUnion H
⊢ x = y

Proof state:
x y : ZFSet.{u_1}
H : {x} = {y}
this : ⋃₀ {x} = ⋃₀ {y} := congr_arg sUnion H
⊢ x = y

Tactic:
rwa [sUnion_singleton, sUnion_singleton] at this

Result:
no goals
-- Mathlib/CategoryTheory/Adhesive.lean
theorem IsPushout.IsVanKampen.isPullback_of_mono_left [Mono f] {H : IsPushout f g h i}
    (H' : H.IsVanKampen) : IsPullback f g h i :=
  ((H' (𝟙 _) g g (𝟙 Y) (𝟙 _) f (𝟙 _) i (IsKernelPair.id_of_mono f)
      (IsPullback.of_vert_isIso ⟨by simp⟩) H.1.flip ⟨rfl⟩ ⟨by simp⟩).mp
    (IsPushout.of_horiz_isIso ⟨by simp⟩)).1.flip

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : Mono f
H : IsPushout f g h i
H' : H.IsVanKampen
⊢ 𝟙 W ≫ g = g ≫ 𝟙 Y

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : Mono f
H : IsPushout f g h i
H' : H.IsVanKampen
⊢ g ≫ 𝟙 Y = 𝟙 W ≫ g

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem card_support_le_one_of_eraseLead_eq_zero (h : f.eraseLead = 0) : #f.support ≤ 1

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
hpz : f = 0
⊢ #f.support ≤ 1

case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
hpz : ¬f = 0
⊢ #f.support ≤ 1

Tactic:
case pos => simp [hpz]

Result:
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
hpz : ¬f = 0
⊢ #f.support ≤ 1

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
hpz : ¬f = 0
⊢ #f.support ≤ 1

Tactic:
case neg => exact le_of_eq (card_support_eq_one_of_eraseLead_eq_zero hpz h)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
hpz : ¬f = 0
⊢ #f.support ≤ 1

Tactic:
exact le_of_eq (card_support_eq_one_of_eraseLead_eq_zero hpz h)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
hpz : f = 0
⊢ #f.support ≤ 1

Tactic:
simp [hpz]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
⊢ #f.support ≤ 1

Tactic:
by_cases hpz : f = 0

Result:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
hpz : f = 0
⊢ #f.support ≤ 1

case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
hpz : ¬f = 0
⊢ #f.support ≤ 1
-- Mathlib/Algebra/Ring/Subsemiring/Basic.lean
theorem map_comap_eq_self
    {f : R →+* S} {t : Subsemiring S} (h : t ≤ f.rangeS) : (t.comap f).map f = t

Proof state:
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
t : Subsemiring S
h : t ≤ f.rangeS
⊢ map f (comap f t) = t

Tactic:
simpa only [inf_of_le_left h] using map_comap_eq f t

Result:
no goals
-- Mathlib/FieldTheory/Fixed.lean
theorem toAlgAut_surjective [Finite G] :
    Function.Surjective (MulSemiringAction.toAlgAut G (FixedPoints.subfield G F) F)

Proof state:
G : Type u_1
F : Type u_2
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
⊢ Function.Surjective ⇑(MulSemiringAction.toAlgAut G (↥(subfield G F)) F)

Tactic:
let f : G →* F ≃ₐ[FixedPoints.subfield G F] F :=
  MulSemiringAction.toAlgAut G (FixedPoints.subfield G F) F

Result:
G : Type u_1
F : Type u_2
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f : G →* F ≃ₐ[↥(subfield G F)] F := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
⊢ Function.Surjective ⇑(MulSemiringAction.toAlgAut G (↥(subfield G F)) F)

Proof state:
case intro
G : Type u_1
F : Type u_2
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f✝ : G →* F ≃ₐ[↥(subfield G F)] F := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_1 := G ⧸ f✝.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f✝)
this : FaithfulSMul Q F
f : F ≃ₐ[↥(subfield G F)] F
q : Q
g : G
hg : (MulSemiringAction.toAlgAut Q (↥(subfield Q F)) F) ↑g = AlgEquiv.ofRingEquiv ⋯
⊢ (MulSemiringAction.toAlgAut G (↥(subfield G F)) F) g = f

Tactic:
rwa [AlgEquiv.ext_iff] at hg ⊢

Result:
no goals

Proof state:
G : Type u_1
F : Type u_2
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f : G →* F ≃ₐ[↥(subfield G F)] F := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_1 := G ⧸ f.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f)
⊢ Function.Surjective ⇑(MulSemiringAction.toAlgAut G (↥(subfield G F)) F)

Tactic:
have : FaithfulSMul Q F := ⟨by
  intro q₁ q₂
  refine Quotient.inductionOn₂' q₁ q₂ (fun g₁ g₂ h ↦ QuotientGroup.eq.mpr ?_)
  rwa [MonoidHom.mem_ker, map_mul, map_inv, inv_mul_eq_one, AlgEquiv.ext_iff]⟩

Result:
G : Type u_1
F : Type u_2
inst✝³ : Group G
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
f : G →* F ≃ₐ[↥(subfield G F)] F := MulSemiringAction.toAlgAut G (↥(subfield G F)) F
Q : Type u_1 := G ⧸ f.ker
x✝ : MulSemiringAction Q F := MulSemiringAction.compHom F (QuotientGroup.kerLift f)
this : FaithfulSMul Q F
⊢ Function.Surjective ⇑(MulSemiringAction.toAlgAut G (↥(subfield G F)) F)
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_bounded_set_le (α : Type u) (c : Cardinal) :
    #{ t : Set α // #t ≤ c } ≤ max #α ℵ₀ ^ c

Proof state:
α : Type u
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ #{ t // #↑t ≤ c }

Tactic:
refine ⟨Embedding.subtypeMap ?_ ?_⟩

Result:
case refine_1
α : Type u
c : Cardinal.{u}
⊢ Set α ↪ Set (ULift.{u, 0} ℕ ⊕ α)

case refine_2
α : Type u
c : Cardinal.{u}
⊢ ∀ ⦃x : Set α⦄, #↑x ≤ c → #↑(?refine_1 x) ≤ c

Proof state:
case refine_1
α : Type u
c : Cardinal.{u}
⊢ Set α ↪ Set (ULift.{u, 0} ℕ ⊕ α)

Tactic:
apply Embedding.image

Result:
case refine_1.f
α : Type u
c : Cardinal.{u}
⊢ α ↪ ULift.{u, 0} ℕ ⊕ α

Proof state:
α : Type u
c : Cardinal.{u}
⊢ #(ULift.{u, 0} ℕ ⊕ α) ^ c ≤ (#α ⊔ ℵ₀) ^ c

Tactic:
rw [max_comm, ← add_eq_max] <;> rfl

Result:
no goals

Proof state:
α : Type u
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ (#α ⊔ ℵ₀) ^ c

Tactic:
trans #{ t : Set ((ULift.{u} ℕ) ⊕ α) // #t ≤ c }

Result:
α : Type u
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ #{ t // #↑t ≤ c }

α : Type u
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ (#α ⊔ ℵ₀) ^ c

Proof state:
case refine_2
α : Type u
c : Cardinal.{u}
⊢ ∀ ⦃x : Set α⦄, #↑x ≤ c → #↑({ toFun := Sum.inr, inj' := ⋯ }.image x) ≤ c

Tactic:
intro s hs

Result:
case refine_2
α : Type u
c : Cardinal.{u}
s : Set α
hs : #↑s ≤ c
⊢ #↑({ toFun := Sum.inr, inj' := ⋯ }.image s) ≤ c

Proof state:
case inj'
α : Type u
c : Cardinal.{u}
⊢ Injective Sum.inr

Tactic:
apply Sum.inr.inj

Result:
no goals

Proof state:
case refine_2
α : Type u
c : Cardinal.{u}
s : Set α
hs : #↑s ≤ c
⊢ #↑({ toFun := Sum.inr, inj' := ⋯ }.image s) ≤ c

Tactic:
exact mk_image_le.trans hs

Result:
no goals

Proof state:
case refine_1.f
α : Type u
c : Cardinal.{u}
⊢ α ↪ ULift.{u, 0} ℕ ⊕ α

Tactic:
use Sum.inr

Result:
case inj'
α : Type u
c : Cardinal.{u}
⊢ Injective Sum.inr

Proof state:
α : Type u
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ (#α ⊔ ℵ₀) ^ c

Tactic:
apply (mk_bounded_set_le_of_infinite ((ULift.{u} ℕ) ⊕ α) c).trans

Result:
α : Type u
c : Cardinal.{u}
⊢ #(ULift.{u, 0} ℕ ⊕ α) ^ c ≤ (#α ⊔ ℵ₀) ^ c
-- Mathlib/Analysis/SpecialFunctions/Arsinh.lean
theorem exp_arsinh (x : ℝ) : exp (arsinh x) = x + √(1 + x ^ 2)

Proof state:
x : ℝ
⊢ rexp (arsinh x) = x + √(1 + x ^ 2)

Tactic:
apply exp_log

Result:
case hx
x : ℝ
⊢ 0 < x + √(1 + x ^ 2)

Proof state:
case hx.h
x : ℝ
⊢ (-x) ^ 2 < 1 + x ^ 2

Tactic:
simp

Result:
no goals

Proof state:
case hx
x : ℝ
⊢ 0 < x + √(1 + x ^ 2)

Tactic:
rw [← neg_lt_iff_pos_add']

Result:
case hx
x : ℝ
⊢ -x < √(1 + x ^ 2)

Proof state:
case hx
x : ℝ
⊢ -x < √(1 + x ^ 2)

Tactic:
apply lt_sqrt_of_sq_lt

Result:
case hx.h
x : ℝ
⊢ (-x) ^ 2 < 1 + x ^ 2
-- Mathlib/Analysis/Analytic/Basic.lean
lemma HasFPowerSeriesWithinAt.congr {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E}
    {x : E} (h : HasFPowerSeriesWithinAt f p s x) (h' : g =ᶠ[𝓝[s] x] f) (h'' : g x = f x) :
    HasFPowerSeriesWithinAt g p s x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
h' : g =ᶠ[𝓝[s] x] f
h'' : g x = f x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
ε : ℝ≥0∞
εpos : ε > 0
hε : EMetric.ball x ε ∩ s ⊆ {y | g y = f y}
r' : ℝ≥0∞ := r ⊓ ε
this : HasFPowerSeriesWithinOnBall f p s x r'
⊢ EqOn g f (s ∩ EMetric.ball x r')

Tactic:
intro z hz

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
h' : g =ᶠ[𝓝[s] x] f
h'' : g x = f x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
ε : ℝ≥0∞
εpos : ε > 0
hε : EMetric.ball x ε ∩ s ⊆ {y | g y = f y}
r' : ℝ≥0∞ := r ⊓ ε
this : HasFPowerSeriesWithinOnBall f p s x r'
z : E
hz : z ∈ s ∩ EMetric.ball x r'
⊢ g z = f z
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive add_zsmul]
lemma zpow_add (a : G) (m n : ℤ) : a ^ (m + n) = a ^ m * a ^ n

Proof state:
case hp
G : Type u_3
inst✝ : Group G
a : G
m : ℤ
n : ℕ
ihn : a ^ (m + ↑n) = a ^ m * a ^ ↑n
⊢ a ^ (m + (↑n + 1)) = a ^ m * a ^ (↑n + 1)

Tactic:
simp only [← Int.add_assoc, zpow_add_one, ihn, mul_assoc]

Result:
no goals

Proof state:
case hz
G : Type u_3
inst✝ : Group G
a : G
m : ℤ
⊢ a ^ (m + 0) = a ^ m * a ^ 0

Tactic:
simp

Result:
no goals

Proof state:
case hn
G : Type u_3
inst✝ : Group G
a : G
m : ℤ
n : ℕ
ihn : a ^ (m + -↑n) = a ^ m * a ^ (-↑n)
⊢ a ^ (m + (-↑n - 1)) = a ^ m * a ^ (-↑n - 1)

Tactic:
rw [zpow_sub_one, ← mul_assoc, ← ihn, ← zpow_sub_one, Int.add_sub_assoc]

Result:
no goals

Proof state:
G : Type u_3
inst✝ : Group G
a : G
m n : ℤ
⊢ a ^ (m + n) = a ^ m * a ^ n

Tactic:
induction n with
| hz => simp
| hp n ihn => simp only [← Int.add_assoc, zpow_add_one, ihn, mul_assoc]
| hn n ihn => rw [zpow_sub_one, ← mul_assoc, ← ihn, ← zpow_sub_one, Int.add_sub_assoc]

Result:
no goals