harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem Module.finrank_eq_zero_of_rank_eq_zero (h : Module.rank R M = 0) :
    finrank R M = 0

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : Module.rank R M = 0
⊢ finrank R M = 0

Tactic:
delta finrank

Result:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : Module.rank R M = 0
⊢ toNat (Module.rank R M) = 0

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : Module.rank R M = 0
⊢ toNat (Module.rank R M) = 0

Tactic:
rw [h, zero_toNat]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem continuousWithinAt_insert [TopologicalSpace Y] [T1Space X]
    {x y : X} {s : Set X} {f : X → Y} :
    ContinuousWithinAt f (insert y s) x ↔ ContinuousWithinAt f s x

Proof state:
case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space X
x y : X
s : Set X
f : X → Y
h : x ≠ y
⊢ ContinuousWithinAt f (insert y s) x ↔ ContinuousWithinAt f s x

Tactic:
simp_rw [ContinuousWithinAt, nhdsWithin_insert_of_ne h]

Result:
no goals

Proof state:
case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space X
x : X
s : Set X
f : X → Y
⊢ ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f s x

Tactic:
exact continuousWithinAt_insert_self

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space X
x y : X
s : Set X
f : X → Y
⊢ ContinuousWithinAt f (insert y s) x ↔ ContinuousWithinAt f s x

Tactic:
rcases eq_or_ne x y with (rfl | h)

Result:
case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space X
x : X
s : Set X
f : X → Y
⊢ ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f s x

case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space X
x y : X
s : Set X
f : X → Y
h : x ≠ y
⊢ ContinuousWithinAt f (insert y s) x ↔ ContinuousWithinAt f s x
-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem familyOfElements_compatible : hx.familyOfElements.Compatible

Proof state:
case mk.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
x : (i : I) → P.obj (op (X i))
hx : Compatible P π x
Z Y✝ : C
i : I
g₁ : Z ⟶ X i
Y : C
j : I
g₂ : Z ⟶ X j
hgf : g₁ ≫ π i = g₂ ≫ π j
⊢ P.map g₁.op (hx.familyOfElements (π i) ⋯) = P.map g₂.op (hx.familyOfElements (π j) ⋯)

Tactic:
simp [hx i j Z g₁ g₂ hgf]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
x : (i : I) → P.obj (op (X i))
hx : Compatible P π x
⊢ hx.familyOfElements.Compatible

Tactic:
rintro Y₁ Y₂ Z g₁ g₂ f₁ f₂ ⟨i⟩ ⟨j⟩ hgf

Result:
case mk.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
x : (i : I) → P.obj (op (X i))
hx : Compatible P π x
Z Y✝ : C
i : I
g₁ : Z ⟶ X i
Y : C
j : I
g₂ : Z ⟶ X j
hgf : g₁ ≫ π i = g₂ ≫ π j
⊢ P.map g₁.op (hx.familyOfElements (π i) ⋯) = P.map g₂.op (hx.familyOfElements (π j) ⋯)
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem IsCycle.cycleOf_eq [DecidableRel f.SameCycle]
    (hf : IsCycle f) (hx : f x ≠ x) : cycleOf f x = f :=
  Equiv.ext fun y =>
    if h : SameCycle f x y then by rw [h.cycleOf_apply]
    else by
      rw [cycleOf_apply_of_not_sameCycle h,
        Classical.not_not.1 (mt ((isCycle_iff_sameCycle hx).1 hf).2 h)]

Proof state:
α : Type u_2
f : Perm α
x : α
inst✝ : DecidableRel f.SameCycle
hf : f.IsCycle
hx : f x ≠ x
y : α
h : ¬f.SameCycle x y
⊢ (f.cycleOf x) y = f y

Tactic:
rw [cycleOf_apply_of_not_sameCycle h,
  Classical.not_not.1 (mt ((isCycle_iff_sameCycle hx).1 hf).2 h)]

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
x : α
inst✝ : DecidableRel f.SameCycle
hf : f.IsCycle
hx : f x ≠ x
y : α
h : f.SameCycle x y
⊢ (f.cycleOf x) y = f y

Tactic:
rw [h.cycleOf_apply]

Result:
no goals
-- Mathlib/Data/Int/Cast/Basic.lean
theorem cast_one : ((1 : ℤ) : R) = 1

Proof state:
R : Type u
inst✝ : AddGroupWithOne R
⊢ ↑1 = 1

Tactic:
erw [cast_natCast, Nat.cast_one]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Hom.lean
theorem comp_id (f : A →ₑ+[φ] B) : f.comp (DistribMulActionHom.id M) = f :=
  ext fun x => by rw [comp_apply, id_apply]

Proof state:
M : Type u_1
inst✝⁵ : Monoid M
N : Type u_2
inst✝⁴ : Monoid N
φ : M →* N
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : DistribMulAction M A
B : Type u_5
inst✝¹ : AddMonoid B
inst✝ : DistribMulAction N B
f : A →ₑ+[φ] B
x : A
⊢ (f.comp (DistribMulActionHom.id M)) x = f x

Tactic:
rw [comp_apply, id_apply]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem inverse_mul_cancel_left (x y : M₀) (h : IsUnit x) : inverse x * (x * y) = y

Proof state:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y : M₀
h : IsUnit x
⊢ inverse x * (x * y) = y

Tactic:
rw [← mul_assoc, inverse_mul_cancel x h, one_mul]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
theorem exists_countablyGenerated_le_of_countablySeparated [m : MeasurableSpace α]
    [h : CountablySeparated α] :
    ∃ m' : MeasurableSpace α, @CountablyGenerated _ m' ∧ @SeparatesPoints _ m' ∧ m' ≤ m

Proof state:
α : Type u_1
m : MeasurableSpace α
h : CountablySeparated α
⊢ ∃ m', CountablyGenerated α ∧ SeparatesPoints α ∧ m' ≤ m

Tactic:
rcases h with ⟨b, bct, hbm, hb⟩

Result:
case mk.mk.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
b : Set (Set α)
bct : b.Countable
hbm : ∀ s ∈ b, MeasurableSet s
hb : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y
⊢ ∃ m', CountablyGenerated α ∧ SeparatesPoints α ∧ m' ≤ m

Proof state:
case mk.mk.intro.intro.intro.refine_2
α : Type u_1
m : MeasurableSpace α
b : Set (Set α)
bct : b.Countable
hbm : ∀ s ∈ b, MeasurableSet s
hb : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y
⊢ ∀ (x y : α), (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) → x = y

Tactic:
exact fun x y hxy ↦ hb _ trivial _ trivial fun _ hs ↦ hxy _ <| measurableSet_generateFrom hs

Result:
no goals

Proof state:
case mk.mk.intro.intro.intro
α : Type u_1
m : MeasurableSpace α
b : Set (Set α)
bct : b.Countable
hbm : ∀ s ∈ b, MeasurableSet s
hb : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y
⊢ ∃ m', CountablyGenerated α ∧ SeparatesPoints α ∧ m' ≤ m

Tactic:
refine ⟨generateFrom b, ?_, ?_, generateFrom_le hbm⟩

Result:
case mk.mk.intro.intro.intro.refine_1
α : Type u_1
m : MeasurableSpace α
b : Set (Set α)
bct : b.Countable
hbm : ∀ s ∈ b, MeasurableSet s
hb : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y
⊢ CountablyGenerated α

case mk.mk.intro.intro.intro.refine_2
α : Type u_1
m : MeasurableSpace α
b : Set (Set α)
bct : b.Countable
hbm : ∀ s ∈ b, MeasurableSet s
hb : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y
⊢ SeparatesPoints α

Proof state:
case mk.mk.intro.intro.intro.refine_1
α : Type u_1
m : MeasurableSpace α
b : Set (Set α)
bct : b.Countable
hbm : ∀ s ∈ b, MeasurableSet s
hb : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y
⊢ CountablyGenerated α

Tactic:
use b

Result:
no goals

Proof state:
case mk.mk.intro.intro.intro.refine_2
α : Type u_1
m : MeasurableSpace α
b : Set (Set α)
bct : b.Countable
hbm : ∀ s ∈ b, MeasurableSet s
hb : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y
⊢ SeparatesPoints α

Tactic:
rw [@separatesPoints_iff]

Result:
case mk.mk.intro.intro.intro.refine_2
α : Type u_1
m : MeasurableSpace α
b : Set (Set α)
bct : b.Countable
hbm : ∀ s ∈ b, MeasurableSet s
hb : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y
⊢ ∀ (x y : α), (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) → x = y
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem lmulEquiv_eq_lidOfCompatibleSMul [CompatibleSMul R S S S] :
    lmulEquiv R S = lidOfCompatibleSMul R S S :=
  AlgEquiv.coe_algHom_injective <| by ext; rfl

Proof state:
case hb.H
R : Type uR
S : Type uS
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : CompatibleSMul R S S S
x✝ : S
⊢ ((AlgHom.restrictScalars R ↑(lmulEquiv R S)).comp includeRight) x✝ =
    ((AlgHom.restrictScalars R ↑(lidOfCompatibleSMul R S S)).comp includeRight) x✝

Tactic:
rfl

Result:
no goals

Proof state:
R : Type uR
S : Type uS
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : CompatibleSMul R S S S
⊢ ↑(lmulEquiv R S) = ↑(lidOfCompatibleSMul R S S)

Tactic:
ext

Result:
case hb.H
R : Type uR
S : Type uS
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : CompatibleSMul R S S S
x✝ : S
⊢ ((AlgHom.restrictScalars R ↑(lmulEquiv R S)).comp includeRight) x✝ =
    ((AlgHom.restrictScalars R ↑(lidOfCompatibleSMul R S S)).comp includeRight) x✝
-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma IsCondKernelCDF.integral
    {f : α × β → StieltjesFunction} (hf : IsCondKernelCDF f κ ν) (a : α) (x : ℝ) :
    ∫ b, f (a, b) x ∂(ν a) = (κ a (univ ×ˢ Iic x)).toReal

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
hf : IsCondKernelCDF f κ ν
a : α
x : ℝ
⊢ ∫ (b : β), ↑(f (a, b)) x ∂ν a = ((κ a) (univ ×ˢ Iic x)).toReal

Tactic:
rw [← hf.setIntegral _ MeasurableSet.univ, Measure.restrict_univ]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem InjOn.imageFactorization_injective (h : InjOn f s) :
    Injective (s.imageFactorization f) :=
  fun ⟨x, hx⟩ ⟨y, hy⟩ h' ↦ by simpa [imageFactorization, h.eq_iff hx hy] using h'

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
x✝¹ x✝ : ↑s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h' : imageFactorization f s ⟨x, hx⟩ = imageFactorization f s ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
simpa [imageFactorization, h.eq_iff hx hy] using h'

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem card_unique [Nonempty α] [Subsingleton α] : Nat.card α = 1

Proof state:
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : Subsingleton α
⊢ Nat.card α = 1

Tactic:
simp [card_eq_one_iff_unique, *]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_const' (c : ε) (h0 : p ≠ 0) (h_top : p ≠ ∞) :
    eLpNorm (fun _ : α => c) p μ = ‖c‖ₑ * μ Set.univ ^ (1 / ENNReal.toReal p)

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
c : ε
h0 : p ≠ 0
h_top : p ≠ ⊤
⊢ eLpNorm (fun x => c) p μ = ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)

Tactic:
simp [eLpNorm_eq_eLpNorm' h0 h_top, eLpNorm'_const, ENNReal.toReal_pos h0 h_top]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem nextCoeffUp_of_constantCoeff_eq_zero (p : R[X]) (hp : coeff p 0 = 0) :
    nextCoeffUp p = p.coeff (p.natTrailingDegree + 1)

Proof state:
case inl
R : Type u
inst✝ : Semiring R
hp : coeff 0 0 = 0
⊢ nextCoeffUp 0 = coeff 0 (natTrailingDegree 0 + 1)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.coeff 0 = 0
⊢ p.nextCoeffUp = p.coeff (p.natTrailingDegree + 1)

Tactic:
obtain rfl | hp₀ := eq_or_ne p 0

Result:
case inl
R : Type u
inst✝ : Semiring R
hp : coeff 0 0 = 0
⊢ nextCoeffUp 0 = coeff 0 (natTrailingDegree 0 + 1)

case inr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.coeff 0 = 0
hp₀ : p ≠ 0
⊢ p.nextCoeffUp = p.coeff (p.natTrailingDegree + 1)

Proof state:
case inr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.coeff 0 = 0
hp₀ : p ≠ 0
⊢ p.nextCoeffUp = p.coeff (p.natTrailingDegree + 1)

Tactic:
rw [nextCoeffUp, if_neg (natTrailingDegree_ne_zero.2 ⟨hp₀, hp⟩)]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma eq_zero_of_double_le (h : 2 * n ≤ n) : n = 0

Proof state:
n : ℕ
h : 2 * n ≤ n
⊢ n = 0

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem totalDegree_add_eq_right_of_totalDegree_lt {p q : MvPolynomial σ R}
    (h : q.totalDegree < p.totalDegree) : (q + p).totalDegree = p.totalDegree

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ (q + p).totalDegree = p.totalDegree

Tactic:
rw [add_comm, totalDegree_add_eq_left_of_totalDegree_lt h]

Result:
no goals
-- Mathlib/Analysis/Matrix.lean
theorem linfty_opNNNorm_diagonal [DecidableEq m] (v : m → α) : ‖diagonal v‖₊ = ‖v‖₊

Proof state:
case e_f.h.refine_2
m : Type u_3
α : Type u_5
inst✝² : Fintype m
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
i : m
⊢ ‖diagonal v i i‖₊ = ‖v i‖₊

Tactic:
rw [diagonal_apply_eq]

Result:
no goals

Proof state:
case e_f.h
m : Type u_3
α : Type u_5
inst✝² : Fintype m
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
i : m
⊢ ∑ j : m, ‖diagonal v i j‖₊ = ‖v i‖₊

Tactic:
refine (Finset.sum_eq_single_of_mem _ (Finset.mem_univ i) fun j _hj hij => ?_).trans ?_

Result:
case e_f.h.refine_1
m : Type u_3
α : Type u_5
inst✝² : Fintype m
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
i j : m
_hj : j ∈ Finset.univ
hij : j ≠ i
⊢ ‖diagonal v i j‖₊ = 0

case e_f.h.refine_2
m : Type u_3
α : Type u_5
inst✝² : Fintype m
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
i : m
⊢ ‖diagonal v i i‖₊ = ‖v i‖₊

Proof state:
m : Type u_3
α : Type u_5
inst✝² : Fintype m
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
⊢ (Finset.univ.sup fun i => ∑ j : m, ‖diagonal v i j‖₊) = Finset.univ.sup fun b => ‖v b‖₊

Tactic:
congr 1 with i : 1

Result:
case e_f.h
m : Type u_3
α : Type u_5
inst✝² : Fintype m
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
i : m
⊢ ∑ j : m, ‖diagonal v i j‖₊ = ‖v i‖₊

Proof state:
case e_f.h.refine_1
m : Type u_3
α : Type u_5
inst✝² : Fintype m
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
i j : m
_hj : j ∈ Finset.univ
hij : j ≠ i
⊢ ‖diagonal v i j‖₊ = 0

Tactic:
rw [diagonal_apply_ne' _ hij, nnnorm_zero]

Result:
no goals

Proof state:
m : Type u_3
α : Type u_5
inst✝² : Fintype m
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
⊢ ‖diagonal v‖₊ = ‖v‖₊

Tactic:
rw [linfty_opNNNorm_def, Pi.nnnorm_def]

Result:
m : Type u_3
α : Type u_5
inst✝² : Fintype m
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq m
v : m → α
⊢ (Finset.univ.sup fun i => ∑ j : m, ‖diagonal v i j‖₊) = Finset.univ.sup fun b => ‖v b‖₊
-- Mathlib/Topology/Order/LowerUpperTopology.lean
lemma isUpper_orderDual [Preorder α] [TopologicalSpace α] : IsUpper αᵒᵈ ↔ IsLower α

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ IsUpper αᵒᵈ ↔ IsLower α

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ IsUpper αᵒᵈ → IsLower α

case mpr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ IsLower α → IsUpper αᵒᵈ

Proof state:
case mpr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ IsLower α → IsUpper αᵒᵈ

Tactic:
apply OrderDual.instIsUpper

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ IsUpper αᵒᵈ → IsLower α

Tactic:
apply OrderDual.instIsLower

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem induction_on {C : CoprodI M → Prop} (m : CoprodI M) (h_one : C 1)
    (h_of : ∀ (i) (m : M i), C (of m)) (h_mul : ∀ x y, C x → C y → C (x * y)) : C m

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
C : CoprodI M → Prop
m : CoprodI M
h_one : C 1
h_of : ∀ (i : ι) (m : M i), C (of m)
h_mul : ∀ (x y : CoprodI M), C x → C y → C (x * y)
⊢ C m

Tactic:
induction m using CoprodI.induction_left with
| one => exact h_one
| mul m x hx => exact h_mul _ _ (h_of _ _) hx

Result:
no goals

Proof state:
case mul
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
C : CoprodI M → Prop
h_one : C 1
h_of : ∀ (i : ι) (m : M i), C (of m)
h_mul : ∀ (x y : CoprodI M), C x → C y → C (x * y)
i✝ : ι
m : M i✝
x : CoprodI M
hx : C x
⊢ C (of m * x)

Tactic:
exact h_mul _ _ (h_of _ _) hx

Result:
no goals

Proof state:
case one
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
C : CoprodI M → Prop
h_one : C 1
h_of : ∀ (i : ι) (m : M i), C (of m)
h_mul : ∀ (x y : CoprodI M), C x → C y → C (x * y)
⊢ C 1

Tactic:
exact h_one

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem inf_sup_left (a b c : α) : a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c :=
  calc
    a ⊓ (b ⊔ c) = a ⊓ (a ⊔ c) ⊓ (b ⊔ c)

Proof state:
α : Type u
inst✝ : DistribLattice α
a b c : α
⊢ (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c) = a ⊓ b ⊔ a ⊓ c

Tactic:
rw [sup_inf_left]

Result:
no goals

Proof state:
α : Type u
inst✝ : DistribLattice α
a b c : α
⊢ a ⊓ (a ⊓ b ⊔ c) = (a ⊔ a ⊓ b) ⊓ (a ⊓ b ⊔ c)

Tactic:
rw [sup_inf_self]

Result:
no goals

Proof state:
α : Type u
inst✝ : DistribLattice α
a b c : α
⊢ a ⊓ (b ⊔ c) = a ⊓ (a ⊔ c) ⊓ (b ⊔ c)

Tactic:
rw [inf_sup_self]

Result:
no goals

Proof state:
α : Type u
inst✝ : DistribLattice α
a b c : α
⊢ a ⊓ (a ⊔ c) ⊓ (b ⊔ c) = a ⊓ (a ⊓ b ⊔ c)

Tactic:
simp only [inf_assoc, sup_inf_right, eq_self_iff_true]

Result:
no goals

Proof state:
α : Type u
inst✝ : DistribLattice α
a b c : α
⊢ (a ⊔ a ⊓ b) ⊓ (a ⊓ b ⊔ c) = (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c)

Tactic:
rw [sup_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
theorem sin_ne_zero_iff {θ : ℂ} : sin θ ≠ 0 ↔ ∀ k : ℤ, θ ≠ k * π

Proof state:
θ : ℂ
⊢ sin θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ ↑k * ↑π

Tactic:
rw [← not_exists, not_iff_not, sin_eq_zero_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/LawfulOperator.lean
theorem denote_mem_prefix {aig : AIG α} {input} (h) :
    ⟦(f aig input).aig, ⟨start, by apply lt_size_of_lt_aig_size; omega⟩, assign⟧
      =
    ⟦aig, ⟨start, h⟩, assign⟧ :=  by
  rw [denote_input_entry ⟨aig, start, h⟩]

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
assign : α → Bool
start : Nat
aig : AIG α
input : β aig
h : start < aig.decls.size
⊢ ⟦assign, { aig := (f aig input).aig, ref := { gate := start, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, hgate := h } }⟧

Tactic:
rw [denote_input_entry ⟨aig, start, h⟩]

Result:
no goals

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
assign : α → Bool
start : Nat
aig : AIG α
input : β aig
h : start < aig.decls.size
⊢ start < (f aig input).aig.decls.size

Tactic:
apply lt_size_of_lt_aig_size

Result:
case h
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
assign : α → Bool
start : Nat
aig : AIG α
input : β aig
h : start < aig.decls.size
⊢ start < aig.decls.size

Proof state:
case h
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
assign : α → Bool
start : Nat
aig : AIG α
input : β aig
h : start < aig.decls.size
⊢ start < aig.decls.size

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem Wbtw.trans_sbtw_right [NoZeroSMulDivisors R V] {w x y z : P} (h₁ : Wbtw R w x z)
    (h₂ : Sbtw R x y z) : Sbtw R w y z

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
w x y z : P
h₁ : Wbtw R z x w
h₂ : Sbtw R x y z
⊢ Sbtw R w y z

Tactic:
rw [sbtw_comm] at *

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
w x y z : P
h₁ : Wbtw R z x w
h₂ : Sbtw R z y x
⊢ Sbtw R z y w

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
w x y z : P
h₁ : Wbtw R z x w
h₂ : Sbtw R z y x
⊢ Sbtw R z y w

Tactic:
exact h₁.trans_sbtw_left h₂

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
w x y z : P
h₁ : Wbtw R w x z
h₂ : Sbtw R x y z
⊢ Sbtw R w y z

Tactic:
rw [wbtw_comm] at *

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
w x y z : P
h₁ : Wbtw R z x w
h₂ : Sbtw R x y z
⊢ Sbtw R w y z
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_insertMany_empty_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
    {l : List ((a : α) × β a)} {k : α}
    (h : (l.map Sigma.fst).contains k = false) :
    (insertMany empty l).1.getKey? k = none

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
k : α
h : (List.map Sigma.fst l).contains k = false
⊢ (empty.insertMany l).val.getKey? k = none

Tactic:
rw [getKey?_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ h]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
k : α
h : (List.map Sigma.fst l).contains k = false
⊢ empty.getKey? k = none

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
k : α
h : (List.map Sigma.fst l).contains k = false
⊢ empty.getKey? k = none

Tactic:
apply getKey?_empty

Result:
no goals
-- Mathlib/InformationTheory/Hamming.lean
theorem hammingDist_pos {x y : ∀ i, β i} : 0 < hammingDist x y ↔ x ≠ y

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ 0 < hammingDist x y ↔ x ≠ y

Tactic:
rw [← hammingDist_ne_zero, iff_not_comm, not_lt, Nat.le_zero]

Result:
no goals
-- Mathlib/GroupTheory/Commutator/Basic.lean
theorem commutatorElement_inv : ⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆

Proof state:
G : Type u_1
inst✝ : Group G
g₁ g₂ : G
⊢ ⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆

Tactic:
simp_rw [commutatorElement_def, mul_inv_rev, inv_inv, mul_assoc]

Result:
no goals
-- Mathlib/Data/List/Range.lean
/-- Any entry of any member of `l.ranges` is strictly smaller than `Nat.sum l`.
See `List.mem_mem_ranges_iff_lt_sum` for the version about `List.sum`. -/
@[deprecated "Use `List.mem_mem_ranges_iff_lt_sum`." (since := "2024-11-18")]
lemma mem_mem_ranges_iff_lt_natSum (l : List ℕ) {n : ℕ} :
    (∃ s ∈ l.ranges, n ∈ s) ↔ n < Nat.sum l

Proof state:
l : List ℕ
n : ℕ
⊢ (∃ s, s ∈ l.ranges ∧ n ∈ s) ↔ n < Nat.sum l

Tactic:
rw [← mem_range, ← ranges_flatten', mem_flatten]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
@[simp] lemma exp_one_pow (n : ℕ) : exp 1 ^ n = exp n

Proof state:
n : ℕ
⊢ rexp 1 ^ n = rexp ↑n

Tactic:
rw [← rpow_natCast, exp_one_rpow]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem continuous_inv' (g : GroupTopology α) :
    haveI := g.toTopologicalSpace
    Continuous (Inv.inv : α → α)

Proof state:
α : Type u
inst✝ : Group α
g : GroupTopology α
this : TopologicalSpace α := g.toTopologicalSpace
⊢ Continuous Inv.inv

Tactic:
haveI := g.toIsTopologicalGroup

Result:
α : Type u
inst✝ : Group α
g : GroupTopology α
this✝ : TopologicalSpace α := g.toTopologicalSpace
this : IsTopologicalGroup α
⊢ Continuous Inv.inv

Proof state:
α : Type u
inst✝ : Group α
g : GroupTopology α
⊢ Continuous Inv.inv

Tactic:
letI := g.toTopologicalSpace

Result:
α : Type u
inst✝ : Group α
g : GroupTopology α
this : TopologicalSpace α := g.toTopologicalSpace
⊢ Continuous Inv.inv

Proof state:
α : Type u
inst✝ : Group α
g : GroupTopology α
this✝ : TopologicalSpace α := g.toTopologicalSpace
this : IsTopologicalGroup α
⊢ Continuous Inv.inv

Tactic:
exact continuous_inv

Result:
no goals