harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mk'_cancel (m : M) (s : S) : mk' f (s • m) s = f m

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ mk' f (s • m) s = f m

Tactic:
delta mk'

Result:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk (s • m) s) = f m

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk (s • m) s) = f m

Tactic:
rw [LocalizedModule.mk_cancel, ← mk'_one S f, fromLocalizedModule_mk,
  Module.End_algebraMap_isUnit_inv_apply_eq_iff, OneMemClass.coe_one, mk'_one, one_smul]

Result:
no goals
-- Mathlib/Probability/Density.lean
theorem _root_.Real.hasPDF_iff_of_aemeasurable [SFinite ℙ] (hX : AEMeasurable X ℙ) :
    HasPDF X ℙ ↔ map X ℙ ≪ volume

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
inst✝ : SFinite ℙ
hX : AEMeasurable X ℙ
⊢ HasPDF X ℙ volume ↔ map X ℙ ≪ volume

Tactic:
rw [Real.hasPDF_iff, and_iff_right hX]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem foldl_eq_foldr [Std.Commutative f] [Std.Associative f] :
    ∀ a l, foldl f a l = foldr f a l
  | _, nil => rfl
  | a, b :: l => by
    simp only [foldr_cons, foldl_eq_of_comm_of_assoc]
    rw [foldl_eq_foldr a l]

Proof state:
α : Type u
f : α → α → α
inst✝¹ : Std.Commutative f
inst✝ : Std.Associative f
a b : α
l : List α
⊢ foldl f a (b :: l) = foldr f a (b :: l)

Tactic:
simp only [foldr_cons, foldl_eq_of_comm_of_assoc]

Result:
α : Type u
f : α → α → α
inst✝¹ : Std.Commutative f
inst✝ : Std.Associative f
a b : α
l : List α
⊢ f b (foldl f a l) = f b (foldr f a l)

Proof state:
α : Type u
f : α → α → α
inst✝¹ : Std.Commutative f
inst✝ : Std.Associative f
a b : α
l : List α
⊢ f b (foldl f a l) = f b (foldr f a l)

Tactic:
rw [foldl_eq_foldr a l]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem range'_subset_right {s m n : Nat} (step0 : 0 < step) :
    range' s m step ⊆ range' s n step ↔ m ≤ n

Proof state:
step s m n : Nat
step0 : 0 < step
⊢ range' s m step ⊆ range' s n step ↔ m ≤ n

Tactic:
refine ⟨fun h => Nat.le_of_not_lt fun hn => ?_, fun h => (range'_sublist_right.2 h).subset⟩

Result:
step s m n : Nat
step0 : 0 < step
h : range' s m step ⊆ range' s n step
hn : n < m
⊢ False

Proof state:
step s m n : Nat
step0 : 0 < step
h : range' s m step ⊆ range' s n step
hn : n < m
i : Nat
h' : i < n
e : s + step * n = s + step * i
⊢ False

Tactic:
exact Nat.ne_of_gt h' (Nat.eq_of_mul_eq_mul_left step0 (Nat.add_left_cancel e))

Result:
no goals

Proof state:
step s m n : Nat
step0 : 0 < step
h : range' s m step ⊆ range' s n step
hn : n < m
⊢ False

Tactic:
have ⟨i, h', e⟩ := mem_range'.1 <| h <| mem_range'.2 ⟨_, hn, rfl⟩

Result:
step s m n : Nat
step0 : 0 < step
h : range' s m step ⊆ range' s n step
hn : n < m
i : Nat
h' : i < n
e : s + step * n = s + step * i
⊢ False
-- Mathlib/NumberTheory/FermatPsp.lean
theorem fermatPsp_base_one {n : ℕ} (h₁ : 1 < n) (h₂ : ¬n.Prime) : FermatPsp n 1

Proof state:
n : ℕ
h₁ : 1 < n
h₂ : ¬Prime n
⊢ n.FermatPsp 1

Tactic:
refine ⟨show n ∣ 1 ^ (n - 1) - 1 from ?_, h₂, h₁⟩

Result:
n : ℕ
h₁ : 1 < n
h₂ : ¬Prime n
⊢ n ∣ 1 ^ (n - 1) - 1

Proof state:
n : ℕ
h₁ : 1 < n
h₂ : ¬Prime n
⊢ n ∣ 1 ^ (n - 1) - 1

Tactic:
exact show 0 = 1 ^ (n - 1) - 1 by norm_num ▸ dvd_zero n

Result:
no goals

Proof state:
n : ℕ
h₁ : 1 < n
h₂ : ¬Prime n
⊢ 0 = 1 ^ (n - 1) - 1

Tactic:
norm_num

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem simpleFunc_bot {α} (f : @SimpleFunc α ⊥ β) [Nonempty β] : ∃ c, ∀ x, f x = c

Proof state:
β : Type u_2
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
hf_meas : ∀ (x : β), MeasurableSet (⇑f ⁻¹' {x})
⊢ ∃ c, ∀ (x : α), f x = c

Tactic:
simp_rw [MeasurableSpace.measurableSet_bot_iff] at hf_meas

Result:
β : Type u_2
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
hf_meas : ∀ (x : β), ⇑f ⁻¹' {x} = ∅ ∨ ⇑f ⁻¹' {x} = univ
⊢ ∃ c, ∀ (x : α), f x = c

Proof state:
β : Type u_2
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
⊢ ∃ c, ∀ (x : α), f x = c

Tactic:
have hf_meas := @SimpleFunc.measurableSet_fiber α _ ⊥ f

Result:
β : Type u_2
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
hf_meas : ∀ (x : β), MeasurableSet (⇑f ⁻¹' {x})
⊢ ∃ c, ∀ (x : α), f x = c

Proof state:
β : Type u_2
α : Type u_5
f : α →ₛ β
inst✝ : Nonempty β
hf_meas : ∀ (x : β), ⇑f ⁻¹' {x} = ∅ ∨ ⇑f ⁻¹' {x} = univ
⊢ ∃ c, ∀ (x : α), f x = c

Tactic:
exact (exists_eq_const_of_preimage_singleton hf_meas).imp fun c hc ↦ congr_fun hc

Result:
no goals
-- Mathlib/Order/Partition/Basic.lean
lemma parts_nonempty (P : Partition s) (hs : s ≠ ⊥) : (P : Set α).Nonempty :=
  nonempty_iff_ne_empty.2 fun hP ↦ by simp [← P.sSup_eq, hP, sSup_empty] at hs

Proof state:
α : Type u_1
s : α
inst✝ : CompleteLattice α
P : Partition s
hs : s ≠ ⊥
hP : ↑P = ∅
⊢ False

Tactic:
simp [← P.sSup_eq, hP, sSup_empty] at hs

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem algebraicIndependent_finset_map_embedding_subtype (s : Set A)
    (li : AlgebraicIndependent R ((↑) : s → A)) (t : Finset s) :
    AlgebraicIndependent R ((↑) : Finset.map (Embedding.subtype s) t → A)

Proof state:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => ⟨↑x, ⋯⟩
⊢ Injective f

Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩

Result:
case mk.mk
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : { x // x ∈ Finset.map (Embedding.subtype s) t } → ↑s := fun x => ⟨↑x, ⋯⟩
x : A
hx : x ∈ Finset.map (Embedding.subtype s) t
y : A
hy : y ∈ Finset.map (Embedding.subtype s) t
⊢ f ⟨x, hx⟩ = f ⟨y, hy⟩ → ⟨x, hx⟩ = ⟨y, hy⟩
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
theorem angle_midpoint_eq_pi (p₁ p₂ : P) (hp₁p₂ : p₁ ≠ p₂) : ∠ p₁ (midpoint ℝ p₁ p₂) p₂ = π

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
hp₁p₂ : p₁ ≠ p₂
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (-(p₁ -ᵥ p₂)) = π

Tactic:
apply angle_self_neg_of_nonzero

Result:
case hx
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
hp₁p₂ : p₁ ≠ p₂
⊢ p₁ -ᵥ p₂ ≠ 0

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
hp₁p₂ : p₁ ≠ p₂
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₂ -ᵥ p₁) = π

Tactic:
rw [← neg_vsub_eq_vsub_rev p₁ p₂]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
hp₁p₂ : p₁ ≠ p₂
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (-(p₁ -ᵥ p₂)) = π

Proof state:
case hx
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
hp₁p₂ : p₁ ≠ p₂
⊢ p₁ -ᵥ p₂ ≠ 0

Tactic:
simpa only [ne_eq, vsub_eq_zero_iff_eq]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
hp₁p₂ : p₁ ≠ p₂
⊢ ∠ p₁ (midpoint ℝ p₁ p₂) p₂ = π

Tactic:
simp only [angle, left_vsub_midpoint, invOf_eq_inv, right_vsub_midpoint, inv_pos, zero_lt_two,
  angle_smul_right_of_pos, angle_smul_left_of_pos]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
hp₁p₂ : p₁ ≠ p₂
⊢ InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₂ -ᵥ p₁) = π
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem isBigO_deriv_ofReal_cpow_const_atTop (c : ℂ) :
    deriv (fun (x : ℝ) => (x : ℂ) ^ c) =O[atTop] fun x => x ^ (c.re - 1)

Proof state:
c : ℂ
⊢ (deriv fun x => ↑x ^ c) =O[atTop] fun x => x ^ (c.re - 1)

Tactic:
obtain rfl | hc := eq_or_ne c 0

Result:
case inl

⊢ (deriv fun x => ↑x ^ 0) =O[atTop] fun x => x ^ (re 0 - 1)

case inr
c : ℂ
hc : c ≠ 0
⊢ (deriv fun x => ↑x ^ c) =O[atTop] fun x => x ^ (c.re - 1)

Proof state:
case inr
c : ℂ
hc : c ≠ 0
⊢ (deriv fun x => ↑x ^ c) =O[atTop] fun x => x ^ (c.re - 1)

Tactic:
exact (isTheta_deriv_ofReal_cpow_const_atTop hc).1

Result:
no goals

Proof state:
case inl

⊢ (deriv fun x => ↑x ^ 0) =O[atTop] fun x => x ^ (re 0 - 1)

Tactic:
simp_rw [cpow_zero, deriv_const', Asymptotics.isBigO_zero]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem powerlt_aleph0 {c : Cardinal} (h : ℵ₀ ≤ c) : c ^< ℵ₀ = c

Proof state:
case a.intro
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
n : ℕ
⊢ c ^ ↑n ≤ c

Tactic:
apply power_nat_le h

Result:
no goals

Proof state:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ^< ℵ₀ = c

Tactic:
apply le_antisymm

Result:
case a
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ^< ℵ₀ ≤ c

case a
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ≤ c ^< ℵ₀

Proof state:
case h.e'_3
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c = c ^ 1

Tactic:
rw [power_one]

Result:
no goals

Proof state:
case a
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
c' : Cardinal.{u_1}
⊢ c' < ℵ₀ → c ^ c' ≤ c

Tactic:
rw [lt_aleph0]

Result:
case a
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
c' : Cardinal.{u_1}
⊢ (∃ n, c' = ↑n) → c ^ c' ≤ c

Proof state:
case a
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ^< ℵ₀ ≤ c

Tactic:
rw [powerlt_le]

Result:
case a
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ ∀ x < ℵ₀, c ^ x ≤ c

Proof state:
case a
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
c' : Cardinal.{u_1}
⊢ (∃ n, c' = ↑n) → c ^ c' ≤ c

Tactic:
rintro ⟨n, rfl⟩

Result:
case a.intro
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
n : ℕ
⊢ c ^ ↑n ≤ c

Proof state:
case a
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ ∀ x < ℵ₀, c ^ x ≤ c

Tactic:
intro c'

Result:
case a
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
c' : Cardinal.{u_1}
⊢ c' < ℵ₀ → c ^ c' ≤ c

Proof state:
case a
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ≤ c ^< ℵ₀

Tactic:
convert le_powerlt c one_lt_aleph0

Result:
case h.e'_3
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c = c ^ 1
-- Mathlib/Data/Nat/Digits.lean
theorem ofDigits_eq_foldr {α : Type*} [Semiring α] (b : α) (L : List ℕ) :
    ofDigits b L = List.foldr (fun x y => ↑x + b * y) 0 L

Proof state:
α : Type u_1
inst✝ : Semiring α
b : α
L : List ℕ
⊢ ofDigits b L = List.foldr (fun x y => ↑x + b * y) 0 L

Tactic:
induction' L with d L ih

Result:
case nil
α : Type u_1
inst✝ : Semiring α
b : α
⊢ ofDigits b [] = List.foldr (fun x y => ↑x + b * y) 0 []

case cons
α : Type u_1
inst✝ : Semiring α
b : α
d : ℕ
L : List ℕ
ih : ofDigits b L = List.foldr (fun x y => ↑x + b * y) 0 L
⊢ ofDigits b (d :: L) = List.foldr (fun x y => ↑x + b * y) 0 (d :: L)

Proof state:
case cons
α : Type u_1
inst✝ : Semiring α
b : α
d : ℕ
L : List ℕ
ih : ofDigits b L = List.foldr (fun x y => ↑x + b * y) 0 L
⊢ ofDigits b (d :: L) = List.foldr (fun x y => ↑x + b * y) 0 (d :: L)

Tactic:
dsimp [ofDigits]

Result:
case cons
α : Type u_1
inst✝ : Semiring α
b : α
d : ℕ
L : List ℕ
ih : ofDigits b L = List.foldr (fun x y => ↑x + b * y) 0 L
⊢ ↑d + b * ofDigits b L = ↑d + b * List.foldr (fun x y => ↑x + b * y) 0 L

Proof state:
case nil
α : Type u_1
inst✝ : Semiring α
b : α
⊢ ofDigits b [] = List.foldr (fun x y => ↑x + b * y) 0 []

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : Semiring α
b : α
d : ℕ
L : List ℕ
ih : ofDigits b L = List.foldr (fun x y => ↑x + b * y) 0 L
⊢ ↑d + b * ofDigits b L = ↑d + b * List.foldr (fun x y => ↑x + b * y) 0 L

Tactic:
rw [ih]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Pointwise.lean
theorem mul_toSubmodule_le (S T : Subalgebra R A) :
    (Subalgebra.toSubmodule S)* (Subalgebra.toSubmodule T) ≤ Subalgebra.toSubmodule (S ⊔ T)

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
y : A
hy : y ∈ toSubmodule S
z : A
hz : z ∈ toSubmodule T
⊢ y * z ∈ toSubmodule (S ⊔ T)

Tactic:
show y * z ∈ S ⊔ T

Result:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
y : A
hy : y ∈ toSubmodule S
z : A
hz : z ∈ toSubmodule T
⊢ y * z ∈ S ⊔ T

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ ∀ m ∈ toSubmodule S, ∀ n ∈ toSubmodule T, m * n ∈ toSubmodule (S ⊔ T)

Tactic:
intro y hy z hz

Result:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
y : A
hy : y ∈ toSubmodule S
z : A
hz : z ∈ toSubmodule T
⊢ y * z ∈ toSubmodule (S ⊔ T)

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ toSubmodule S * toSubmodule T ≤ toSubmodule (S ⊔ T)

Tactic:
rw [Submodule.mul_le]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ ∀ m ∈ toSubmodule S, ∀ n ∈ toSubmodule T, m * n ∈ toSubmodule (S ⊔ T)

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
y : A
hy : y ∈ toSubmodule S
z : A
hz : z ∈ toSubmodule T
⊢ y * z ∈ S ⊔ T

Tactic:
exact mul_mem (Algebra.mem_sup_left hy) (Algebra.mem_sup_right hz)

Result:
no goals
-- Mathlib/AlgebraicGeometry/Restrict.lean
lemma resLE_preimage (f : X ⟶ Y) {U : Y.Opens} {V : X.Opens} (e : V ≤ f ⁻¹ᵁ U)
    (O : U.toScheme.Opens) :
    f.resLE U V e ⁻¹ᵁ O = V.ι ⁻¹ᵁ (f ⁻¹ᵁ U.ι ''ᵁ O)

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U).Opens
⊢ resLE f U V e ⁻¹ᵁ O = V.ι ⁻¹ᵁ f ⁻¹ᵁ U.ι ''ᵁ O

Tactic:
rw [← preimage_comp, ← resLE_comp_ι f e, preimage_comp, preimage_image_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem forM_congr [Monad m] {as bs : Array α} (w : as = bs)
    {f : α → m PUnit} :
    forM as f = forM bs f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
inst✝ : Monad m
as bs : Array α
w : as = bs
f : α → m PUnit
⊢ forM as f = forM bs f

Tactic:
cases as <;> cases bs

Result:
case mk.mk
m : Type u_1 → Type u_2
α : Type u_3
inst✝ : Monad m
f : α → m PUnit
toList✝¹ toList✝ : List α
w : { toList := toList✝¹ } = { toList := toList✝ }
⊢ forM { toList := toList✝¹ } f = forM { toList := toList✝ } f

Proof state:
case mk.mk
m : Type u_1 → Type u_2
α : Type u_3
inst✝ : Monad m
f : α → m PUnit
toList✝¹ toList✝ : List α
w : { toList := toList✝¹ } = { toList := toList✝ }
⊢ forM { toList := toList✝¹ } f = forM { toList := toList✝ } f

Tactic:
simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem Decidable.not_or_self (p : Prop) [h : Decidable p] : ¬p ∨ p

Proof state:
p : Prop
h : Decidable p
⊢ ¬p ∨ p

Tactic:
cases h <;> simp [*]

Result:
no goals
-- Mathlib/Analysis/RCLike/Inner.lean
@[simp] lemma wInner_neg_right (w : ι → ℝ) (f g : ∀ i, E i) : ⟪f, -g⟫_[𝕜, w] = -⟪f, g⟫_[𝕜, w]

Proof state:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : RCLike 𝕜
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (E i)
w : ι → ℝ
f g : (i : ι) → E i
⊢ wInner w f (-g) = -wInner w f g

Tactic:
simp [wInner]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
theorem pow_sub_pow_eq_sub_mul_geomSum :
    a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
n : ℕ
⊢ a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n

Tactic:
induction' n with n ih

Result:
case zero
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
n : ℕ
⊢ a ^ (0 + 1) - b ^ (0 + 1) = (a - b) * geomSum a b 0

case succ
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
n✝ n : ℕ
ih : a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * geomSum a b (n + 1)

Proof state:
case zero
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
n : ℕ
⊢ a ^ (0 + 1) - b ^ (0 + 1) = (a - b) * geomSum a b 0

Tactic:
simp [geomSum]

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : LinearOrderedCommRing α
a b : α
n✝ n : ℕ
ih : a ^ (n + 1) - b ^ (n + 1) = (a - b) * geomSum a b n
⊢ a ^ (n + 1 + 1) - b ^ (n + 1 + 1) = (a - b) * geomSum a b (n + 1)

Tactic:
rw [geomSum, mul_add, mul_comm a, ← mul_assoc, ← ih,
  sub_mul, sub_mul, ← pow_succ, ← pow_succ', mul_comm, sub_add_sub_cancel]

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
lemma not_commutative : ∀ {n : ℕ}, n ≠ 1 → n ≠ 2 →
    ¬Std.Commutative fun (x y : DihedralGroup n) => x * y
  | 0, _, _ => fun ⟨h'⟩ ↦ by simpa using h' (r 1) (sr 0)
  | n + 3, _, _ => by
    rintro ⟨h'⟩
    specialize h' (r 1) (sr 0)
    rw [r_mul_sr, zero_sub, sr_mul_r, zero_add, sr.injEq, neg_eq_iff_add_eq_zero,
      one_add_one_eq_two, ← ZMod.val_eq_zero, ZMod.val_two_eq_two_mod] at h'
    simpa using Nat.le_of_dvd Nat.zero_lt_two <| Nat.dvd_of_mod_eq_zero h'

Proof state:
case mk
n : ℕ
x✝¹ : n + 3 ≠ 1
x✝ : n + 3 ≠ 2
h' : r 1 * sr 0 = sr 0 * r 1
⊢ False

Tactic:
rw [r_mul_sr, zero_sub, sr_mul_r, zero_add, sr.injEq, neg_eq_iff_add_eq_zero,
  one_add_one_eq_two, ← ZMod.val_eq_zero, ZMod.val_two_eq_two_mod] at h'

Result:
case mk
n : ℕ
x✝¹ : n + 3 ≠ 1
x✝ : n + 3 ≠ 2
h' : 2 % (n + 3) = 0
⊢ False

Proof state:
case mk
n : ℕ
x✝¹ : n + 3 ≠ 1
x✝ : n + 3 ≠ 2
h' : 2 % (n + 3) = 0
⊢ False

Tactic:
simpa using Nat.le_of_dvd Nat.zero_lt_two <| Nat.dvd_of_mod_eq_zero h'

Result:
no goals

Proof state:
case mk
n : ℕ
x✝¹ : n + 3 ≠ 1
x✝ : n + 3 ≠ 2
h' : ∀ (a b : DihedralGroup (n + 3)), a * b = b * a
⊢ False

Tactic:
specialize h' (r 1) (sr 0)

Result:
case mk
n : ℕ
x✝¹ : n + 3 ≠ 1
x✝ : n + 3 ≠ 2
h' : r 1 * sr 0 = sr 0 * r 1
⊢ False

Proof state:
x✝² : 0 ≠ 1
x✝¹ : 0 ≠ 2
x✝ : Std.Commutative fun x y => x * y
h' : ∀ (a b : DihedralGroup 0), a * b = b * a
⊢ False

Tactic:
simpa using h' (r 1) (sr 0)

Result:
no goals

Proof state:
n : ℕ
x✝¹ : n + 3 ≠ 1
x✝ : n + 3 ≠ 2
⊢ ¬Std.Commutative fun x y => x * y

Tactic:
rintro ⟨h'⟩

Result:
case mk
n : ℕ
x✝¹ : n + 3 ≠ 1
x✝ : n + 3 ≠ 2
h' : ∀ (a b : DihedralGroup (n + 3)), a * b = b * a
⊢ False
-- Mathlib/Algebra/Polynomial/Mirror.lean
theorem mirror_natDegree : p.mirror.natDegree = p.natDegree

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
a✝ : Nontrivial R
⊢ p.mirror.natDegree = p.natDegree

Tactic:
rw [mirror, natDegree_mul', reverse_natDegree, natDegree_X_pow,
  tsub_add_cancel_of_le p.natTrailingDegree_le_natDegree]

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
a✝ : Nontrivial R
⊢ p.reverse.leadingCoeff * (X ^ p.natTrailingDegree).leadingCoeff ≠ 0

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p = 0
⊢ p.mirror.natDegree = p.natDegree

Tactic:
rw [hp, mirror_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p.mirror.natDegree = p.natDegree

Tactic:
by_cases hp : p = 0

Result:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p = 0
⊢ p.mirror.natDegree = p.natDegree

case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
⊢ p.mirror.natDegree = p.natDegree

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
a✝ : Nontrivial R
⊢ p.reverse.leadingCoeff * (X ^ p.natTrailingDegree).leadingCoeff ≠ 0

Tactic:
rwa [leadingCoeff_X_pow, mul_one, reverse_leadingCoeff, Ne, trailingCoeff_eq_zero]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
⊢ p.mirror.natDegree = p.natDegree

Tactic:
nontriviality R

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : ¬p = 0
a✝ : Nontrivial R
⊢ p.mirror.natDegree = p.natDegree
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem dropLast_replicate (n) (a : α) : dropLast (replicate n a) = replicate (n - 1) a

Proof state:
α : Type u_1
n✝ : Nat
a : α
n : Nat
⊢ (replicate (n + 2) a).dropLast = replicate (n + 2 - 1) a

Tactic:
rw [replicate_succ, dropLast_cons_of_ne_nil, dropLast_replicate]

Result:
α : Type u_1
n✝ : Nat
a : α
n : Nat
⊢ a :: replicate (n + 1 - 1) a = replicate (n + 2 - 1) a

α : Type u_1
n✝ : Nat
a : α
n : Nat
⊢ replicate (n + 1) a ≠ []

Proof state:
α : Type u_1
n : Nat
a : α
⊢ (replicate 0 a).dropLast = replicate (0 - 1) a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
⊢ (replicate 1 a).dropLast = replicate (1 - 1) a

Tactic:
simp [replicate_succ]

Result:
no goals

Proof state:
α : Type u_1
n✝ : Nat
a : α
n : Nat
⊢ a :: replicate (n + 1 - 1) a = replicate (n + 2 - 1) a

Tactic:
simp [replicate_succ]

Result:
no goals

Proof state:
α : Type u_1
n✝ : Nat
a : α
n : Nat
⊢ replicate (n + 1) a ≠ []

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Pairwise.lean
theorem pairwise_push {as : Array α} :
    (as.push a).Pairwise R ↔ as.Pairwise R ∧ (∀ x ∈ as, R x a)

Proof state:
α : Type u_1
a : α
R : α → α → Prop
as : Array α
⊢ Pairwise R (as.push a) ↔ Pairwise R as ∧ ∀ (x : α), x ∈ as → R x a

Tactic:
unfold Pairwise

Result:
α : Type u_1
a : α
R : α → α → Prop
as : Array α
⊢ List.Pairwise R (as.push a).toList ↔ List.Pairwise R as.toList ∧ ∀ (x : α), x ∈ as → R x a

Proof state:
α : Type u_1
a : α
R : α → α → Prop
as : Array α
⊢ List.Pairwise R (as.push a).toList ↔ List.Pairwise R as.toList ∧ ∀ (x : α), x ∈ as → R x a

Tactic:
simp [← mem_toList, push_toList, List.pairwise_append, List.pairwise_singleton,
  List.mem_singleton]

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem Perm.kunion_right {l₁ l₂ : List (Sigma β)} (p : l₁ ~ l₂) (l) :
    kunion l₁ l ~ kunion l₂ l

Proof state:
case trans
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₁ l₂ : List (Sigma β)
l₁✝ l₂✝ l₃✝ : List (Sigma β)
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih₁₂ : ∀ (l : List (Sigma β)), l₁✝.kunion l ~ l₂✝.kunion l
ih₂₃ : ∀ (l : List (Sigma β)), l₂✝.kunion l ~ l₃✝.kunion l
l : List (Sigma β)
⊢ l₁✝.kunion l ~ l₃✝.kunion l

Tactic:
exact Perm.trans (ih₁₂ l) (ih₂₃ l)

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₁ l₂ l : List (Sigma β)
⊢ [].kunion l ~ [].kunion l

Tactic:
rfl

Result:
no goals

Proof state:
case swap
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₁ l₂ : List (Sigma β)
s₁ s₂ : Sigma β
l✝ : List (Sigma β)
l : List (Sigma β)
⊢ (s₂ :: s₁ :: l✝).kunion l ~ (s₁ :: s₂ :: l✝).kunion l

Tactic:
simp [kerase_comm, Perm.swap]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₁ l₂ : List (Sigma β)
p : l₁ ~ l₂
l : List (Sigma β)
⊢ l₁.kunion l ~ l₂.kunion l

Tactic:
induction p generalizing l with
| nil => rfl
| cons hd _ ih =>
  simp [ih (List.kerase _ _), Perm.cons]
| swap s₁ s₂ l => simp [kerase_comm, Perm.swap]
| trans _ _ ih₁₂ ih₂₃ => exact Perm.trans (ih₁₂ l) (ih₂₃ l)

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₁ l₂ : List (Sigma β)
hd : Sigma β
l₁✝ l₂✝ : List (Sigma β)
a✝ : l₁✝ ~ l₂✝
ih : ∀ (l : List (Sigma β)), l₁✝.kunion l ~ l₂✝.kunion l
l : List (Sigma β)
⊢ (hd :: l₁✝).kunion l ~ (hd :: l₂✝).kunion l

Tactic:
simp [ih (List.kerase _ _), Perm.cons]

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem liftRel_pure (R : α → β → Prop) (a : α) (b : β) :
    LiftRel R (pure a) (pure b) ↔ R a b

Proof state:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
⊢ LiftRel R (pure a) (pure b) ↔ R a b

Tactic:
rw [liftRel_pure_left]

Result:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
⊢ (∃ b_1, b_1 ∈ pure b ∧ R a b_1) ↔ R a b

Proof state:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
x✝ : ∃ b_1, b_1 ∈ pure b ∧ R a b_1
b' : β
mb' : b' ∈ pure b
ab' : R a b'
⊢ R a b

Tactic:
rwa [eq_of_pure_mem mb'] at ab'

Result:
no goals

Proof state:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
⊢ (∃ b_1, b_1 ∈ pure b ∧ R a b_1) ↔ R a b

Tactic:
exact ⟨fun ⟨b', mb', ab'⟩ => by rwa [eq_of_pure_mem mb'] at ab', fun ab => ⟨_, ret_mem _, ab⟩⟩

Result:
no goals