harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Kaehler/Basic.lean
theorem KaehlerDifferential.kerTotal_mkQ_single_smul (r : R) (x y) : (y𝖣r • x) = r • y𝖣x

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
x y : S
this : SMulZeroClass R S := inferInstance
⊢ (y𝖣r • x) = r • y𝖣x

Tactic:
rw [Algebra.smul_def, KaehlerDifferential.kerTotal_mkQ_single_mul,
  KaehlerDifferential.kerTotal_mkQ_single_algebraMap, add_zero, ← LinearMap.map_smul_of_tower,
  Finsupp.smul_single, mul_comm, Algebra.smul_def]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
x y : S
⊢ (y𝖣r • x) = r • y𝖣x

Tactic:
letI : SMulZeroClass R S := inferInstance

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
x y : S
this : SMulZeroClass R S := inferInstance
⊢ (y𝖣r • x) = r • y𝖣x
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
theorem scaleRoots_eval₂_eq_zero_of_eval₂_div_eq_zero {p : S[X]} {f : S →+* K}
    (hf : Function.Injective f) {r s : S} (hr : eval₂ f (f r / f s) p = 0)
    (hs : s ∈ nonZeroDivisors S) : eval₂ f (f r) (scaleRoots p s) = 0

Proof state:
S : Type u_2
K : Type u_4
inst✝¹ : Semiring S
inst✝ : Field K
p : S[X]
f : S →+* K
hf : Function.Injective ⇑f
r s : S
hr : eval₂ f (f r / f s) p = 0
hs : s ∈ nonZeroDivisors S
⊢ eval₂ f (f r) (p.scaleRoots s) = 0

Tactic:
nontriviality S using Subsingleton.eq_zero (_ : S)

Result:
S : Type u_2
K : Type u_4
inst✝¹ : Semiring S
inst✝ : Field K
p : S[X]
f : S →+* K
hf : Function.Injective ⇑f
r s : S
hr : eval₂ f (f r / f s) p = 0
hs : s ∈ nonZeroDivisors S
a✝ : Nontrivial S
⊢ eval₂ f (f r) (p.scaleRoots s) = 0

Proof state:
case h.e'_2.h.e'_6
S : Type u_2
K : Type u_4
inst✝¹ : Semiring S
inst✝ : Field K
p : S[X]
f : S →+* K
hf : Function.Injective ⇑f
r s : S
hr : eval₂ f (f r / f s) p = 0
hs : s ∈ nonZeroDivisors S
a✝ : Nontrivial S
⊢ f r = f s * (f r / f s)

Tactic:
rw [← mul_div_assoc, mul_comm, mul_div_cancel_right₀]

Result:
case h.e'_2.h.e'_6.hb
S : Type u_2
K : Type u_4
inst✝¹ : Semiring S
inst✝ : Field K
p : S[X]
f : S →+* K
hf : Function.Injective ⇑f
r s : S
hr : eval₂ f (f r / f s) p = 0
hs : s ∈ nonZeroDivisors S
a✝ : Nontrivial S
⊢ f s ≠ 0

Proof state:
S : Type u_2
K : Type u_4
inst✝¹ : Semiring S
inst✝ : Field K
p : S[X]
f : S →+* K
hf : Function.Injective ⇑f
r s : S
hr : eval₂ f (f r / f s) p = 0
hs : s ∈ nonZeroDivisors S
a✝ : Nontrivial S
⊢ eval₂ f (f r) (p.scaleRoots s) = 0

Tactic:
convert @scaleRoots_eval₂_eq_zero _ _ _ _ p f _ s hr

Result:
case h.e'_2.h.e'_6
S : Type u_2
K : Type u_4
inst✝¹ : Semiring S
inst✝ : Field K
p : S[X]
f : S →+* K
hf : Function.Injective ⇑f
r s : S
hr : eval₂ f (f r / f s) p = 0
hs : s ∈ nonZeroDivisors S
a✝ : Nontrivial S
⊢ f r = f s * (f r / f s)

Proof state:
case h.e'_2.h.e'_6.hb
S : Type u_2
K : Type u_4
inst✝¹ : Semiring S
inst✝ : Field K
p : S[X]
f : S →+* K
hf : Function.Injective ⇑f
r s : S
hr : eval₂ f (f r / f s) p = 0
hs : s ∈ nonZeroDivisors S
a✝ : Nontrivial S
⊢ f s ≠ 0

Tactic:
exact map_ne_zero_of_mem_nonZeroDivisors _ hf hs

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem HasStrictFDerivAt.hasFDerivAt (hf : HasStrictFDerivAt f f' x) :
    HasFDerivAt f f' x :=
  .of_isLittleOTVS <| by
    simpa only using hf.isLittleOTVS.comp_tendsto (tendsto_id.prod_mk_nhds tendsto_const_nhds)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
⊢ (fun x' => f x' - f x - f' (x' - x)) =o[𝕜;𝓝 x] fun x' => x' - x

Tactic:
simpa only using hf.isLittleOTVS.comp_tendsto (tendsto_id.prod_mk_nhds tendsto_const_nhds)

Result:
no goals
-- Mathlib/NumberTheory/Pell.lean
theorem eq_zero_of_d_neg (h₀ : d < 0) (a : Solution₁ d) : a.x = 0 ∨ a.y = 0

Proof state:
d : ℤ
h₀ : d < 0
a : Solution₁ d
h : a.x ≠ 0 ∧ a.y ≠ 0
h1 : 0 < a.x ^ 2
⊢ a.x ^ 2 - d * a.y ^ 2 ≠ 1

Tactic:
have h2 := sq_pos_of_ne_zero h.2

Result:
d : ℤ
h₀ : d < 0
a : Solution₁ d
h : a.x ≠ 0 ∧ a.y ≠ 0
h1 : 0 < a.x ^ 2
h2 : 0 < a.y ^ 2
⊢ a.x ^ 2 - d * a.y ^ 2 ≠ 1

Proof state:
d : ℤ
h₀ : d < 0
a : Solution₁ d
h : a.x ≠ 0 ∧ a.y ≠ 0
⊢ a.x ^ 2 - d * a.y ^ 2 ≠ 1

Tactic:
have h1 := sq_pos_of_ne_zero h.1

Result:
d : ℤ
h₀ : d < 0
a : Solution₁ d
h : a.x ≠ 0 ∧ a.y ≠ 0
h1 : 0 < a.x ^ 2
⊢ a.x ^ 2 - d * a.y ^ 2 ≠ 1

Proof state:
d : ℤ
h₀ : d < 0
a : Solution₁ d
h : a.x ≠ 0 ∧ a.y ≠ 0
h1 : 0 < a.x ^ 2
h2 : 0 < a.y ^ 2
⊢ a.x ^ 2 - d * a.y ^ 2 ≠ 1

Tactic:
nlinarith

Result:
no goals

Proof state:
d : ℤ
h₀ : d < 0
a : Solution₁ d
h : a.x ^ 2 - d * a.y ^ 2 = 1
⊢ a.x = 0 ∨ a.y = 0

Tactic:
contrapose! h

Result:
d : ℤ
h₀ : d < 0
a : Solution₁ d
h : a.x ≠ 0 ∧ a.y ≠ 0
⊢ a.x ^ 2 - d * a.y ^ 2 ≠ 1

Proof state:
d : ℤ
h₀ : d < 0
a : Solution₁ d
⊢ a.x = 0 ∨ a.y = 0

Tactic:
have h := a.prop

Result:
d : ℤ
h₀ : d < 0
a : Solution₁ d
h : a.x ^ 2 - d * a.y ^ 2 = 1
⊢ a.x = 0 ∨ a.y = 0
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Perm.lean
theorem perm_insertP (p : α → Bool) (a l) : insertP p a l ~ a :: l

Proof state:
case cons.h_2
α : Type u_1
p : α → Bool
a head✝ : α
tail✝ : List α
ih : insertP p a tail✝ ~ a :: tail✝
c✝ : Bool
heq✝ : p head✝ = false
⊢ insertP.loop p a tail✝ [head✝] ~ a :: head✝ :: tail✝

Tactic:
rw [insertP_loop, reverseAux, reverseAux]

Result:
case cons.h_2
α : Type u_1
p : α → Bool
a head✝ : α
tail✝ : List α
ih : insertP p a tail✝ ~ a :: tail✝
c✝ : Bool
heq✝ : p head✝ = false
⊢ head✝ :: insertP p a tail✝ ~ a :: head✝ :: tail✝

Proof state:
case cons
α : Type u_1
p : α → Bool
a head✝ : α
tail✝ : List α
ih : insertP p a tail✝ ~ a :: tail✝
⊢ (match p head✝ with
    | true => a :: head✝ :: tail✝
    | false => insertP.loop p a tail✝ [head✝]) ~
    a :: head✝ :: tail✝

Tactic:
split

Result:
case cons.h_1
α : Type u_1
p : α → Bool
a head✝ : α
tail✝ : List α
ih : insertP p a tail✝ ~ a :: tail✝
c✝ : Bool
heq✝ : p head✝ = true
⊢ a :: head✝ :: tail✝ ~ a :: head✝ :: tail✝

case cons.h_2
α : Type u_1
p : α → Bool
a head✝ : α
tail✝ : List α
ih : insertP p a tail✝ ~ a :: tail✝
c✝ : Bool
heq✝ : p head✝ = false
⊢ insertP.loop p a tail✝ [head✝] ~ a :: head✝ :: tail✝

Proof state:
case cons.h_2
α : Type u_1
p : α → Bool
a head✝ : α
tail✝ : List α
ih : insertP p a tail✝ ~ a :: tail✝
c✝ : Bool
heq✝ : p head✝ = false
⊢ head✝ :: insertP p a tail✝ ~ a :: head✝ :: tail✝

Tactic:
exact Perm.trans (Perm.cons _ ih) (Perm.swap ..)

Result:
no goals

Proof state:
case cons.h_1
α : Type u_1
p : α → Bool
a head✝ : α
tail✝ : List α
ih : insertP p a tail✝ ~ a :: tail✝
c✝ : Bool
heq✝ : p head✝ = true
⊢ a :: head✝ :: tail✝ ~ a :: head✝ :: tail✝

Tactic:
exact Perm.refl ..

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Constructions.lean
lemma orthogonal_comm {v w : ℙ F (m → F)} : orthogonal v w ↔ orthogonal w v

Proof state:
F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v w : ℙ F (m → F)
⊢ v.orthogonal w ↔ w.orthogonal v

Tactic:
induction v with | h v hv => induction w with | h w hw =>
rw [orthogonal_mk hv hw, orthogonal_mk hw hv, dotProduct_comm]

Result:
no goals

Proof state:
case h.h
F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
v : m → F
hv : v ≠ 0
w : m → F
hw : w ≠ 0
⊢ (mk F v hv).orthogonal (mk F w hw) ↔ (mk F w hw).orthogonal (mk F v hv)

Tactic:
rw [orthogonal_mk hv hw, orthogonal_mk hw hv, dotProduct_comm]

Result:
no goals

Proof state:
case h
F : Type u_1
inst✝¹ : Field F
m : Type u_2
inst✝ : Fintype m
w : ℙ F (m → F)
v : m → F
hv : v ≠ 0
⊢ (mk F v hv).orthogonal w ↔ w.orthogonal (mk F v hv)

Tactic:
induction w with | h w hw =>
rw [orthogonal_mk hv hw, orthogonal_mk hw hv, dotProduct_comm]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem mul_eq_right_iff_opow_omega0_dvd {a b : Ordinal} : a * b = b ↔ a ^ ω ∣ b

Proof state:
case inr.refine_1.inl
a b : Ordinal.{u_1}
ha : 0 < a
hab✝ : a * (b % a ^ ω) = b % a ^ ω
hab : b % a ^ ω = 0
⊢ b % a ^ ω = 0

Tactic:
exact hab

Result:
no goals

Proof state:
a b : Ordinal.{u_1}
⊢ a * b = b ↔ a ^ ω ∣ b

Tactic:
rcases eq_zero_or_pos a with ha | ha

Result:
case inl
a b : Ordinal.{u_1}
ha : a = 0
⊢ a * b = b ↔ a ^ ω ∣ b

case inr
a b : Ordinal.{u_1}
ha : 0 < a
⊢ a * b = b ↔ a ^ ω ∣ b

Proof state:
case inl
a b : Ordinal.{u_1}
ha : a = 0
⊢ a * b = b ↔ a ^ ω ∣ b

Tactic:
rw [ha, zero_mul, zero_opow omega0_ne_zero, zero_dvd_iff]

Result:
case inl
a b : Ordinal.{u_1}
ha : a = 0
⊢ 0 = b ↔ b = 0

Proof state:
case inl
a b : Ordinal.{u_1}
ha : a = 0
⊢ 0 = b ↔ b = 0

Tactic:
exact eq_comm

Result:
no goals

Proof state:
case inr.refine_1.inr
a b : Ordinal.{u_1}
ha : 0 < a
hab✝ : a * (b % a ^ ω) = b % a ^ ω
hab : a ^ ω ≤ b % a ^ ω
⊢ b % a ^ ω = 0

Tactic:
refine (not_lt_of_le hab (mod_lt b (opow_ne_zero ω ?_))).elim

Result:
case inr.refine_1.inr
a b : Ordinal.{u_1}
ha : 0 < a
hab✝ : a * (b % a ^ ω) = b % a ^ ω
hab : a ^ ω ≤ b % a ^ ω
⊢ a ≠ 0

Proof state:
case inr.refine_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * (b % a ^ ω) = b % a ^ ω
⊢ b % a ^ ω = 0

Tactic:
rcases eq_zero_or_opow_omega0_le_of_mul_eq_right hab with hab | hab

Result:
case inr.refine_1.inl
a b : Ordinal.{u_1}
ha : 0 < a
hab✝ : a * (b % a ^ ω) = b % a ^ ω
hab : b % a ^ ω = 0
⊢ b % a ^ ω = 0

case inr.refine_1.inr
a b : Ordinal.{u_1}
ha : 0 < a
hab✝ : a * (b % a ^ ω) = b % a ^ ω
hab : a ^ ω ≤ b % a ^ ω
⊢ b % a ^ ω = 0

Proof state:
case inr.refine_2
a b : Ordinal.{u_1}
ha : 0 < a
h : a ^ ω ∣ b
⊢ a * b = b

Tactic:
obtain ⟨c, hc⟩ := h

Result:
case inr.refine_2.intro
a b : Ordinal.{u_1}
ha : 0 < a
c : Ordinal.{u_1}
hc : b = a ^ ω * c
⊢ a * b = b

Proof state:
case inr.refine_1.inr
a b : Ordinal.{u_1}
ha : 0 < a
hab✝ : a * (b % a ^ ω) = b % a ^ ω
hab : a ^ ω ≤ b % a ^ ω
⊢ a ≠ 0

Tactic:
rwa [← Ordinal.pos_iff_ne_zero]

Result:
no goals

Proof state:
case inr.refine_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * b = b
⊢ a ^ ω ∣ b

Tactic:
rw [dvd_iff_mod_eq_zero]

Result:
case inr.refine_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * b = b
⊢ b % a ^ ω = 0

Proof state:
case inr.refine_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * b = b
⊢ b % a ^ ω = 0

Tactic:
rw [← div_add_mod b (a ^ ω), mul_add, ← mul_assoc, ← opow_one_add, one_add_omega0,
  add_left_cancel_iff] at hab

Result:
case inr.refine_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * (b % a ^ ω) = b % a ^ ω
⊢ b % a ^ ω = 0

Proof state:
case inr
a b : Ordinal.{u_1}
ha : 0 < a
⊢ a * b = b ↔ a ^ ω ∣ b

Tactic:
refine ⟨fun hab => ?_, fun h => ?_⟩

Result:
case inr.refine_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * b = b
⊢ a ^ ω ∣ b

case inr.refine_2
a b : Ordinal.{u_1}
ha : 0 < a
h : a ^ ω ∣ b
⊢ a * b = b

Proof state:
case inr.refine_2.intro
a b : Ordinal.{u_1}
ha : 0 < a
c : Ordinal.{u_1}
hc : b = a ^ ω * c
⊢ a * b = b

Tactic:
rw [hc, ← mul_assoc, ← opow_one_add, one_add_omega0]

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem tail_pmap {p : α → Prop} (f : (a : α) → p a → β) (v : Vector α (n + 1))
    (hp : ∀ x ∈ v.toList, p x) :
    (v.pmap f hp).tail = v.tail.pmap f (fun x hx ↦ hp _ <| by
      rw [← cons_head_tail v, toList_cons, List.mem_cons]; exact .inr hx)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ x ∈ v.toList, p x
x : α
hx : x ∈ v.tail.toList
⊢ x = v.head ∨ x ∈ v.tail.toList

Tactic:
exact .inr hx

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ x ∈ v.toList, p x
⊢ (pmap f v hp).tail = pmap f v.tail ⋯

Tactic:
obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v

Result:
case intro.intro
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ x ∈ v.toList, p x
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (pmap f v hp).tail = pmap f v.tail ⋯

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ x ∈ v.toList, p x
x : α
hx : x ∈ v.tail.toList
⊢ x ∈ v.toList

Tactic:
rw [← cons_head_tail v, toList_cons, List.mem_cons]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ x ∈ v.toList, p x
x : α
hx : x ∈ v.tail.toList
⊢ x = v.head ∨ x ∈ v.tail.toList

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ x ∈ v.toList, p x
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (pmap f v hp).tail = pmap f v.tail ⋯

Tactic:
simp_rw [h, pmap_cons, tail_cons]

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem map_div {B : Type*} [CommSemiring B] [Algebra R B] (I J : Submodule R A)
    (h : A ≃ₐ[R] B) : (I / J).map h.toLinearMap = I.map h.toLinearMap / J.map h.toLinearMap

Proof state:
case h.e'_5.a
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
hx : ∀ (y : B), (∃ y_1 ∈ J, h.toLinearMap y_1 = y) → ∃ y_1 ∈ I, h.toLinearMap y_1 = x * y
z : A
hz : z ∈ J
xz : A
xz_mem : xz ∈ I
hxz : h xz = x * h z
⊢ x * h z = h xz

Tactic:
rw [hxz]

Result:
no goals

Proof state:
case h.e'_5
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
hx : ∀ (y : B), (∃ y_1 ∈ J, h.toLinearMap y_1 = y) → ∃ y_1 ∈ I, h.toLinearMap y_1 = x * y
z : A
hz : z ∈ J
xz : A
xz_mem : xz ∈ I
hxz : h.toLinearMap xz = x * h z
⊢ h.symm x * z = xz

Tactic:
apply h.injective

Result:
case h.e'_5.a
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
hx : ∀ (y : B), (∃ y_1 ∈ J, h.toLinearMap y_1 = y) → ∃ y_1 ∈ I, h.toLinearMap y_1 = x * y
z : A
hz : z ∈ J
xz : A
xz_mem : xz ∈ I
hxz : h.toLinearMap xz = x * h z
⊢ h (h.symm x * z) = h xz

Proof state:
case h.mpr
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
hx : ∀ (y : B), (∃ y_1 ∈ J, h.toLinearMap y_1 = y) → ∃ y_1 ∈ I, h.toLinearMap y_1 = x * y
⊢ ∃ y, (∀ y_1 ∈ J, y * y_1 ∈ I) ∧ h.toLinearMap y = x

Tactic:
refine ⟨h.symm x, fun z hz => ?_, h.apply_symm_apply x⟩

Result:
case h.mpr
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
hx : ∀ (y : B), (∃ y_1 ∈ J, h.toLinearMap y_1 = y) → ∃ y_1 ∈ I, h.toLinearMap y_1 = x * y
z : A
hz : z ∈ J
⊢ h.symm x * z ∈ I
-- Mathlib/GroupTheory/Index.lean
theorem index_ne_zero_of_finite [hH : Finite (G ⧸ H)] : H.index ≠ 0

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Finite (G ⧸ H)
⊢ H.index ≠ 0

Tactic:
cases nonempty_fintype (G ⧸ H)

Result:
case intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Finite (G ⧸ H)
val✝ : Fintype (G ⧸ H)
⊢ H.index ≠ 0

Proof state:
case intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Finite (G ⧸ H)
val✝ : Fintype (G ⧸ H)
⊢ H.index ≠ 0

Tactic:
rw [index_eq_card]

Result:
case intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Finite (G ⧸ H)
val✝ : Fintype (G ⧸ H)
⊢ Nat.card (G ⧸ H) ≠ 0

Proof state:
case intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : Finite (G ⧸ H)
val✝ : Fintype (G ⧸ H)
⊢ Nat.card (G ⧸ H) ≠ 0

Tactic:
exact Nat.card_pos.ne'

Result:
no goals
-- Mathlib/Data/W/Cardinal.lean
theorem cardinalMk_le_of_le' {κ : Cardinal.{max u v}}
    (hκ : (sum fun a : α => κ ^ lift.{u} #(β a)) ≤ κ) :
    #(WType β) ≤ κ

Proof state:
case h
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : (sum fun a => lift.{v, max v u} #γ ^ lift.{max u v, v} #(β a)) ≤ #γ
⊢ #(WType β) ≤ #γ

Tactic:
simp_rw [← mk_arrow, ← mk_sigma, le_def] at hκ

Result:
case h
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : Nonempty ((i : α) × (β i → γ) ↪ γ)
⊢ #(WType β) ≤ #γ

Proof state:
case h
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : Nonempty ((i : α) × (β i → γ) ↪ γ)
⊢ #(WType β) ≤ #γ

Tactic:
obtain ⟨hκ⟩ := hκ

Result:
case h.intro
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : (i : α) × (β i → γ) ↪ γ
⊢ #(WType β) ≤ #γ

Proof state:
case h.intro
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : (i : α) × (β i → γ) ↪ γ
⊢ #(WType β) ≤ #γ

Tactic:
exact Cardinal.mk_le_of_injective (elim_injective _ hκ.1 hκ.2)

Result:
no goals

Proof state:
α : Type u
β : α → Type v
κ : Cardinal.{max u v}
hκ : (sum fun a => κ ^ lift.{u, v} #(β a)) ≤ κ
⊢ #(WType β) ≤ κ

Tactic:
induction' κ using Cardinal.inductionOn with γ

Result:
case h
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : (sum fun a => #γ ^ lift.{u, v} #(β a)) ≤ #γ
⊢ #(WType β) ≤ #γ

Proof state:
case h
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : (sum fun a => #γ ^ lift.{u, v} #(β a)) ≤ #γ
⊢ #(WType β) ≤ #γ

Tactic:
simp_rw [← lift_umax.{v, u}] at hκ

Result:
case h
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : (sum fun a => #γ ^ lift.{max u v, v} #(β a)) ≤ #γ
⊢ #(WType β) ≤ #γ

Proof state:
case h
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : (sum fun a => #γ ^ lift.{max u v, v} #(β a)) ≤ #γ
⊢ #(WType β) ≤ #γ

Tactic:
nth_rewrite 1 [← lift_id'.{v, u} #γ] at hκ

Result:
case h
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : (sum fun a => lift.{v, max v u} #γ ^ lift.{max u v, v} #(β a)) ≤ #γ
⊢ #(WType β) ≤ #γ
-- Mathlib/CategoryTheory/Functor/Currying.lean
lemma uncurry_obj_curry_obj (F : B × C ⥤ D) : uncurry.obj (curry.obj F) = F :=
  Functor.ext (by simp) (fun ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ ⟨f₁, f₂⟩ => by
    dsimp
    simp only [← F.map_comp, Category.id_comp, Category.comp_id, prod_comp])

Proof state:
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F : B × C ⥤ D
x✝² x✝¹ : B × C
x₁ : B
x₂ : C
y₁ : B
y₂ : C
x✝ : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ (uncurry.obj (curry.obj F)).map (f₁, f₂) = eqToHom ⋯ ≫ F.map (f₁, f₂) ≫ eqToHom ⋯

Tactic:
dsimp

Result:
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F : B × C ⥤ D
x✝² x✝¹ : B × C
x₁ : B
x₂ : C
y₁ : B
y₂ : C
x✝ : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ F.map (f₁, 𝟙 x₂) ≫ F.map (𝟙 y₁, f₂) = 𝟙 (F.obj (x₁, x₂)) ≫ F.map (f₁, f₂) ≫ 𝟙 (F.obj (y₁, y₂))

Proof state:
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F : B × C ⥤ D
⊢ ∀ (X : B × C), (uncurry.obj (curry.obj F)).obj X = F.obj X

Tactic:
simp

Result:
no goals

Proof state:
B : Type u₁
inst✝² : Category.{v₁, u₁} B
C : Type u₂
inst✝¹ : Category.{v₂, u₂} C
D : Type u₃
inst✝ : Category.{v₃, u₃} D
F : B × C ⥤ D
x✝² x✝¹ : B × C
x₁ : B
x₂ : C
y₁ : B
y₂ : C
x✝ : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ F.map (f₁, 𝟙 x₂) ≫ F.map (𝟙 y₁, f₂) = 𝟙 (F.obj (x₁, x₂)) ≫ F.map (f₁, f₂) ≫ 𝟙 (F.obj (y₁, y₂))

Tactic:
simp only [← F.map_comp, Category.id_comp, Category.comp_id, prod_comp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem val_add_one_of_lt {n : Nat} {i : Fin n.succ} (h : i < last _) : (i + 1).1 = i + 1

Proof state:
n : Nat
i : Fin (Nat.succ 0)
h : i < last 0
⊢ ↑(i + 1) = ↑i + 1

Tactic:
cases h

Result:
no goals

Proof state:
n✝ n : Nat
i : Fin (n + 1).succ
h : i < last (n + 1)
⊢ ↑i + 1 < (n + 1).succ

Tactic:
exact Nat.succ_lt_succ h

Result:
no goals

Proof state:
n✝ n : Nat
i : Fin (n + 1).succ
h : i < last (n + 1)
⊢ ↑(i + 1) = ↑i + 1

Tactic:
rw [val_add, val_one, Nat.mod_eq_of_lt (by exact Nat.succ_lt_succ h)]

Result:
no goals

Proof state:
n : Nat
i : Fin n.succ
h : i < last n
⊢ ↑(i + 1) = ↑i + 1

Tactic:
match n with
| 0 => cases h
| n+1 => rw [val_add, val_one, Nat.mod_eq_of_lt (by exact Nat.succ_lt_succ h)]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_union_add_inter' (hs : MeasurableSet s) (t : Set α) :
    μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t

Tactic:
simpa only [union_comm, inter_comm, add_comm] using restrict_union_add_inter t hs

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Covolume.lean
theorem covolume_eq_det_inv {ι : Type*} [Fintype ι] [DecidableEq ι] (L : Submodule ℤ (ι → ℝ))
    [DiscreteTopology L] [IsZLattice ℝ L] (b : Basis ι ℤ L) :
    covolume L = |(LinearEquiv.det (b.ofZLatticeBasis ℝ L).equivFun : ℝ)|⁻¹

Proof state:
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
⊢ Subtype.val ∘ ⇑b = ⇑(Basis.ofZLatticeBasis ℝ L b)

Tactic:
ext

Result:
case h.h
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
x✝¹ x✝ : ι
⊢ (Subtype.val ∘ ⇑b) x✝¹ x✝ = (Basis.ofZLatticeBasis ℝ L b) x✝¹ x✝

Proof state:
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
⊢ |(LinearMap.det ↑((Basis.ofZLatticeBasis ℝ L b).equiv (Pi.basisFun ℝ ι) (Equiv.refl ι)))⁻¹| =
    |(LinearMap.det ↑(Basis.ofZLatticeBasis ℝ L b).equivFun)⁻¹|

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
⊢ covolume L volume = |↑(LinearEquiv.det (Basis.ofZLatticeBasis ℝ L b).equivFun)|⁻¹

Tactic:
rw [covolume_eq_det L b, ← Pi.basisFun_det_apply, show (((↑) : L → _) ∘ ⇑b) =
  (b.ofZLatticeBasis ℝ) by ext; simp, ← Basis.det_inv, ← abs_inv, Units.val_inv_eq_inv_val,
  IsUnit.unit_spec, ← Basis.det_basis, LinearEquiv.coe_det]

Result:
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
⊢ |(LinearMap.det ↑((Basis.ofZLatticeBasis ℝ L b).equiv (Pi.basisFun ℝ ι) (Equiv.refl ι)))⁻¹| =
    |(LinearMap.det ↑(Basis.ofZLatticeBasis ℝ L b).equivFun)⁻¹|

Proof state:
case h.h
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
x✝¹ x✝ : ι
⊢ (Subtype.val ∘ ⇑b) x✝¹ x✝ = (Basis.ofZLatticeBasis ℝ L b) x✝¹ x✝

Tactic:
simp

Result:
no goals