harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem lie_comm : ⁅I, J⁆ = ⁅J, I⁆

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I, J⁆ ≤ ⁅J, I⁆

Tactic:
rw [lieIdeal_oper_eq_span, lieSpan_le]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑⁅J, I⁆

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ ∀ (I J : LieIdeal R L), ⁅I, J⁆ ≤ ⁅J, I⁆

Tactic:
intro I J

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I, J⁆ ≤ ⁅J, I⁆

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ ∀ (I J : LieIdeal R L), ⁅I, J⁆ ≤ ⁅J, I⁆

Tactic:
clear! I J

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ ∀ (I J : LieIdeal R L), ⁅I, J⁆ ≤ ⁅J, I⁆

Proof state:
case intro.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
x : L
y : ↥I
z : ↥J
h : ⁅↑y, ↑z⁆ = x
⊢ ⁅↑y, ↑z⁆ ∈ ↑⁅J, I⁆

Tactic:
rw [← lie_skew, ← lie_neg, ← LieSubmodule.coe_neg]

Result:
case intro.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
x : L
y : ↥I
z : ↥J
h : ⁅↑y, ↑z⁆ = x
⊢ ⁅↑z, ↑(-y)⁆ ∈ ↑⁅J, I⁆

Proof state:
case intro.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
x : L
y : ↥I
z : ↥J
h : ⁅↑y, ↑z⁆ = x
⊢ ⁅↑z, ↑(-y)⁆ ∈ ↑⁅J, I⁆

Tactic:
apply lie_coe_mem_lie

Result:
no goals

Proof state:
case intro.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
x : L
y : ↥I
z : ↥J
h : ⁅↑y, ↑z⁆ = x
⊢ x ∈ ↑⁅J, I⁆

Tactic:
rw [← h]

Result:
case intro.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
x : L
y : ↥I
z : ↥J
h : ⁅↑y, ↑z⁆ = x
⊢ ⁅↑y, ↑z⁆ ∈ ↑⁅J, I⁆

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ {x | ∃ x_1 n, ⁅↑x_1, ↑n⁆ = x} ⊆ ↑⁅J, I⁆

Tactic:
rintro x ⟨y, z, h⟩

Result:
case intro.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
x : L
y : ↥I
z : ↥J
h : ⁅↑y, ↑z⁆ = x
⊢ x ∈ ↑⁅J, I⁆

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I, J⁆ = ⁅J, I⁆

Tactic:
suffices ∀ I J : LieIdeal R L, ⁅I, J⁆ ≤ ⁅J, I⁆ by exact le_antisymm (this I J) (this J I)

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ ∀ (I J : LieIdeal R L), ⁅I, J⁆ ≤ ⁅J, I⁆

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
this : ∀ (I J : LieIdeal R L), ⁅I, J⁆ ≤ ⁅J, I⁆
⊢ ⁅I, J⁆ = ⁅J, I⁆

Tactic:
exact le_antisymm (this I J) (this J I)

Result:
no goals
-- Mathlib/Algebra/Group/Units/Defs.lean
@[to_additive] lemma isUnit_iff_eq_one [Subsingleton Mˣ] {x : M} : IsUnit x ↔ x = 1 :=
  ⟨fun ⟨u, hu⟩ ↦ by rw [← hu, Subsingleton.elim u 1, Units.val_one], fun h ↦ h ▸ isUnit_one⟩

Proof state:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x : M
x✝ : IsUnit x
u : Mˣ
hu : ↑u = x
⊢ x = 1

Tactic:
rw [← hu, Subsingleton.elim u 1, Units.val_one]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem coeff_eq_zero_of_lt_order {x : HahnSeries Γ R} {i : Γ} (hi : i < x.order) :
    x.coeff i = 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
i : Γ
hi : i < x.order
⊢ x.coeff i = 0

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Result:
case inl
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
i : Γ
hi : i < order 0
⊢ coeff 0 i = 0

case inr
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
i : Γ
hi : i < x.order
hx : x ≠ 0
⊢ x.coeff i = 0

Proof state:
case inl
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
i : Γ
hi : i < order 0
⊢ coeff 0 i = 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
i : Γ
hi : i < x.order
hx : x ≠ 0
⊢ x.coeff i = 0

Tactic:
contrapose! hi

Result:
case inr
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
i : Γ
hx : x ≠ 0
hi : x.coeff i ≠ 0
⊢ ¬i < x.order

Proof state:
case inr
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬i < ⋯.min ⋯

Tactic:
exact Set.IsWF.not_lt_min _ _ hi

Result:
no goals

Proof state:
case inr
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬i < x.order

Tactic:
rw [order_of_ne hx]

Result:
case inr
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬i < ⋯.min ⋯

Proof state:
case inr
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
i : Γ
hx : x ≠ 0
hi : x.coeff i ≠ 0
⊢ ¬i < x.order

Tactic:
rw [← mem_support] at hi

Result:
case inr
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬i < x.order
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem mul_rpow_of_nonneg (x y : ℝ≥0∞) {z : ℝ} (hz : 0 ≤ z) : (x * y) ^ z = x ^ z * y ^ z

Proof state:
x y : ℝ≥0∞
z : ℝ
hz : 0 ≤ z
⊢ (x * y) ^ z = x ^ z * y ^ z

Tactic:
simp [hz.not_lt, mul_rpow_eq_ite]

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem span_sum : Set.range (eval C) = Set.range (Sum.elim
    (fun (l : GoodProducts (π C (ord I · < o))) ↦ Products.eval C l.1)
    (fun (l : MaxProducts C ho) ↦ Products.eval C l.1))

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ Set.range (eval C) = Set.range (Sum.elim (fun l => Products.eval C ↑l) fun l => Products.eval C ↑l)

Tactic:
rw [← sum_equiv_comp_eval_eq_elim C hsC ho, Equiv.toFun_as_coe,
  EquivLike.range_comp (e := sum_equiv C hsC ho)]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem compl_eq_iff_isCompl : xᶜ = y ↔ IsCompl x y :=
  ⟨fun h => by
    rw [← h]
    exact isCompl_compl, IsCompl.compl_eq⟩

Proof state:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : xᶜ = y
⊢ IsCompl x xᶜ

Tactic:
exact isCompl_compl

Result:
no goals

Proof state:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : xᶜ = y
⊢ IsCompl x y

Tactic:
rw [← h]

Result:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : xᶜ = y
⊢ IsCompl x xᶜ
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem tan_angle_sub_mul_norm_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x ≠ 0 ∨ y = 0) :
    Real.tan (angle x (x - y)) * ‖x‖ = ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y = 0
⊢ Real.tan (angle x (x - y)) * ‖x‖ = ‖y‖

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0 ∨ y = 0
⊢ Real.tan (angle x (x - y)) * ‖x‖ = ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0 ∨ -y = 0
⊢ Real.tan (angle x (x - y)) * ‖x‖ = ‖y‖

Tactic:
rw [sub_eq_add_neg, tan_angle_add_mul_norm_of_inner_eq_zero h h0, norm_neg]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0 ∨ y = 0
⊢ Real.tan (angle x (x - y)) * ‖x‖ = ‖y‖

Tactic:
rw [← neg_eq_zero] at h0

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0 ∨ -y = 0
⊢ Real.tan (angle x (x - y)) * ‖x‖ = ‖y‖
-- Mathlib/Algebra/Homology/SingleHomology.lean
@[reassoc (attr := simp)]
lemma singleObjHomologySelfIso_inv_homologyι :
    (singleObjHomologySelfIso _ _ _).inv ≫ ((single C c j).obj A).homologyι j =
      (singleObjOpcyclesSelfIso _ _ _).hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ (singleObjHomologySelfIso c j A).inv ≫ ((single C c j).obj A).homologyι j = (singleObjOpcyclesSelfIso c j A).hom

Tactic:
rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom,
  singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc, homology_π_ι,
  singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom]

Result:
no goals
-- Mathlib/Data/Finsupp/SMulWithZero.lean
theorem support_smul [AddMonoid M] [SMulZeroClass R M] {b : R} {g : α →₀ M} :
    (b • g).support ⊆ g.support := fun a => by
  simp only [smul_apply, mem_support_iff, Ne]
  exact mt fun h => h.symm ▸ smul_zero _

Proof state:
α : Type u_1
M : Type u_5
R : Type u_11
inst✝¹ : AddMonoid M
inst✝ : SMulZeroClass R M
b : R
g : α →₀ M
a : α
⊢ a ∈ (b • g).support → a ∈ g.support

Tactic:
simp only [smul_apply, mem_support_iff, Ne]

Result:
α : Type u_1
M : Type u_5
R : Type u_11
inst✝¹ : AddMonoid M
inst✝ : SMulZeroClass R M
b : R
g : α →₀ M
a : α
⊢ ¬b • g a = 0 → ¬g a = 0

Proof state:
α : Type u_1
M : Type u_5
R : Type u_11
inst✝¹ : AddMonoid M
inst✝ : SMulZeroClass R M
b : R
g : α →₀ M
a : α
⊢ ¬b • g a = 0 → ¬g a = 0

Tactic:
exact mt fun h => h.symm ▸ smul_zero _

Result:
no goals
-- Mathlib/Algebra/Lie/SkewAdjoint.lean
theorem Matrix.isSkewAdjoint_bracket {A B : Matrix n n R} (hA : A ∈ skewAdjointMatricesSubmodule J)
    (hB : B ∈ skewAdjointMatricesSubmodule J) : ⁅A, B⁆ ∈ skewAdjointMatricesSubmodule J

Proof state:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : Aᵀ * J = J * -A
hB : Bᵀ * J = J * -B
⊢ J * -B * -A - J * -A * -B = J * -(A * B - B * A)

Tactic:
noncomm_ring

Result:
no goals

Proof state:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hB : J.IsSkewAdjoint B
hA : Aᵀ * J = J * -A
⊢ ⁅A, B⁆ᵀ * J = J * -⁅A, B⁆

Tactic:
change Bᵀ * J = J * (-B) at hB

Result:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : Aᵀ * J = J * -A
hB : Bᵀ * J = J * -B
⊢ ⁅A, B⁆ᵀ * J = J * -⁅A, B⁆

Proof state:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : J.IsSkewAdjoint A
hB : J.IsSkewAdjoint B
⊢ ⁅A, B⁆ᵀ * J = J * -⁅A, B⁆

Tactic:
change Aᵀ * J = J * (-A) at hA

Result:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hB : J.IsSkewAdjoint B
hA : Aᵀ * J = J * -A
⊢ ⁅A, B⁆ᵀ * J = J * -⁅A, B⁆

Proof state:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : Aᵀ * J = J * -A
hB : Bᵀ * J = J * -B
⊢ ⁅A, B⁆ᵀ * J = J * -⁅A, B⁆

Tactic:
rw [Matrix.lie_transpose, LieRing.of_associative_ring_bracket,
  LieRing.of_associative_ring_bracket, sub_mul, mul_assoc, mul_assoc, hA, hB, ← mul_assoc,
  ← mul_assoc, hA, hB]

Result:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : Aᵀ * J = J * -A
hB : Bᵀ * J = J * -B
⊢ J * -B * -A - J * -A * -B = J * -(A * B - B * A)

Proof state:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : J.IsSkewAdjoint A
hB : J.IsSkewAdjoint B
⊢ J.IsSkewAdjoint ⁅A, B⁆

Tactic:
change ⁅A, B⁆ᵀ * J = J * (-⁅A, B⁆)

Result:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : J.IsSkewAdjoint A
hB : J.IsSkewAdjoint B
⊢ ⁅A, B⁆ᵀ * J = J * -⁅A, B⁆

Proof state:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : A ∈ skewAdjointMatricesSubmodule J
hB : B ∈ skewAdjointMatricesSubmodule J
⊢ ⁅A, B⁆ ∈ skewAdjointMatricesSubmodule J

Tactic:
simp only [mem_skewAdjointMatricesSubmodule] at *

Result:
R : Type u
n : Type w
inst✝² : CommRing R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
J A B : Matrix n n R
hA : J.IsSkewAdjoint A
hB : J.IsSkewAdjoint B
⊢ J.IsSkewAdjoint ⁅A, B⁆
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem inv_mul_le_iff_le_mul' : c⁻¹ * a ≤ b ↔ a ≤ b * c

Proof state:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c : α
⊢ c⁻¹ * a ≤ b ↔ a ≤ b * c

Tactic:
rw [inv_mul_le_iff_le_mul, mul_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem finStronglyMeasurable_zero {α β} {m : MeasurableSpace α} {μ : Measure α} [Zero β]
    [TopologicalSpace β] : FinStronglyMeasurable (0 : α → β) μ :=
  ⟨0, by
    simp only [Pi.zero_apply, SimpleFunc.coe_zero, support_zero', measure_empty,
      zero_lt_top, forall_const],
    fun _ => tendsto_const_nhds⟩

Proof state:
α : Type u_5
β : Type u_6
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
⊢ ∀ (n : ℕ), μ (support ⇑(0 n)) < ⊤

Tactic:
simp only [Pi.zero_apply, SimpleFunc.coe_zero, support_zero', measure_empty,
  zero_lt_top, forall_const]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_eq_iff {a b : Nat} :
    gcd a b = g ↔ g ∣ a ∧ g ∣ b ∧ (∀ c, c ∣ a → c ∣ b → c ∣ g)

Proof state:
case mpr.intro.intro.a
g a b : Nat
ha : g ∣ a
hb : g ∣ b
hc : ∀ (c : Nat), c ∣ a → c ∣ b → c ∣ g
⊢ g ∣ a.gcd b

Tactic:
exact Nat.dvd_gcd ha hb

Result:
no goals

Proof state:
case mp
a b : Nat
⊢ a.gcd b ∣ a ∧ a.gcd b ∣ b ∧ ∀ (c : Nat), c ∣ a → c ∣ b → c ∣ a.gcd b

Tactic:
exact ⟨gcd_dvd_left _ _, gcd_dvd_right _ _, fun _ => Nat.dvd_gcd⟩

Result:
no goals

Proof state:
case mpr
g a b : Nat
⊢ (g ∣ a ∧ g ∣ b ∧ ∀ (c : Nat), c ∣ a → c ∣ b → c ∣ g) → a.gcd b = g

Tactic:
rintro ⟨ha, hb, hc⟩

Result:
case mpr.intro.intro
g a b : Nat
ha : g ∣ a
hb : g ∣ b
hc : ∀ (c : Nat), c ∣ a → c ∣ b → c ∣ g
⊢ a.gcd b = g

Proof state:
g a b : Nat
⊢ a.gcd b = g ↔ g ∣ a ∧ g ∣ b ∧ ∀ (c : Nat), c ∣ a → c ∣ b → c ∣ g

Tactic:
constructor

Result:
case mp
g a b : Nat
⊢ a.gcd b = g → g ∣ a ∧ g ∣ b ∧ ∀ (c : Nat), c ∣ a → c ∣ b → c ∣ g

case mpr
g a b : Nat
⊢ (g ∣ a ∧ g ∣ b ∧ ∀ (c : Nat), c ∣ a → c ∣ b → c ∣ g) → a.gcd b = g

Proof state:
case mpr.intro.intro.a.a
g a b : Nat
ha : g ∣ a
hb : g ∣ b
hc : ∀ (c : Nat), c ∣ a → c ∣ b → c ∣ g
⊢ a.gcd b ∣ b

Tactic:
exact gcd_dvd_right a b

Result:
no goals

Proof state:
case mpr.intro.intro
g a b : Nat
ha : g ∣ a
hb : g ∣ b
hc : ∀ (c : Nat), c ∣ a → c ∣ b → c ∣ g
⊢ a.gcd b = g

Tactic:
apply Nat.dvd_antisymm

Result:
case mpr.intro.intro.a
g a b : Nat
ha : g ∣ a
hb : g ∣ b
hc : ∀ (c : Nat), c ∣ a → c ∣ b → c ∣ g
⊢ a.gcd b ∣ g

case mpr.intro.intro.a
g a b : Nat
ha : g ∣ a
hb : g ∣ b
hc : ∀ (c : Nat), c ∣ a → c ∣ b → c ∣ g
⊢ g ∣ a.gcd b

Proof state:
case mpr.intro.intro.a.a
g a b : Nat
ha : g ∣ a
hb : g ∣ b
hc : ∀ (c : Nat), c ∣ a → c ∣ b → c ∣ g
⊢ a.gcd b ∣ a

Tactic:
exact gcd_dvd_left a b

Result:
no goals

Proof state:
case mp
g a b : Nat
⊢ a.gcd b = g → g ∣ a ∧ g ∣ b ∧ ∀ (c : Nat), c ∣ a → c ∣ b → c ∣ g

Tactic:
rintro rfl

Result:
case mp
a b : Nat
⊢ a.gcd b ∣ a ∧ a.gcd b ∣ b ∧ ∀ (c : Nat), c ∣ a → c ∣ b → c ∣ a.gcd b

Proof state:
case mpr.intro.intro.a
g a b : Nat
ha : g ∣ a
hb : g ∣ b
hc : ∀ (c : Nat), c ∣ a → c ∣ b → c ∣ g
⊢ a.gcd b ∣ g

Tactic:
apply hc

Result:
case mpr.intro.intro.a.a
g a b : Nat
ha : g ∣ a
hb : g ∣ b
hc : ∀ (c : Nat), c ∣ a → c ∣ b → c ∣ g
⊢ a.gcd b ∣ a

case mpr.intro.intro.a.a
g a b : Nat
ha : g ∣ a
hb : g ∣ b
hc : ∀ (c : Nat), c ∣ a → c ∣ b → c ∣ g
⊢ a.gcd b ∣ b
-- Mathlib/Topology/Instances/AddCircle.lean
theorem liftIco_zero_continuous [TopologicalSpace B] {f : 𝕜 → B} (hf : f 0 = f p)
    (hc : ContinuousOn f <| Icc 0 p) : Continuous (liftIco p 0 f) :=
  liftIco_continuous (by rwa [zero_add] : f 0 = f (0 + p)) (by rwa [zero_add])

Proof state:
𝕜 : Type u_1
B : Type u_2
inst✝⁴ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f 0 = f p
hc : ContinuousOn f (Icc 0 p)
⊢ f 0 = f (0 + p)

Tactic:
rwa [zero_add]

Result:
no goals

Proof state:
𝕜 : Type u_1
B : Type u_2
inst✝⁴ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f 0 = f p
hc : ContinuousOn f (Icc 0 p)
⊢ ContinuousOn f (Icc 0 (0 + p))

Tactic:
rwa [zero_add]

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorPower/Basic.lean
@[simp]
lemma alternatingMapLinearEquiv_symm_apply (F : ⋀[R]^n M →ₗ[R] N) (m : Fin n → M) :
    alternatingMapLinearEquiv.symm F m = F.compAlternatingMap (ιMulti R n) m

Proof state:
case intro
R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
m : Fin n → M
f : M [⋀^Fin n]→ₗ[R] N
⊢ (alternatingMapLinearEquiv.symm (alternatingMapLinearEquiv f)) m =
    ((alternatingMapLinearEquiv f).compAlternatingMap (ιMulti R n)) m

Tactic:
simp only [LinearEquiv.symm_apply_apply, alternatingMapLinearEquiv_comp_ιMulti]

Result:
no goals

Proof state:
R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
F : ↥(⋀[R]^n M) →ₗ[R] N
m : Fin n → M
⊢ (alternatingMapLinearEquiv.symm F) m = (F.compAlternatingMap (ιMulti R n)) m

Tactic:
obtain ⟨f, rfl⟩ := alternatingMapLinearEquiv.surjective F

Result:
case intro
R : Type u
inst✝⁴ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
m : Fin n → M
f : M [⋀^Fin n]→ₗ[R] N
⊢ (alternatingMapLinearEquiv.symm (alternatingMapLinearEquiv f)) m =
    ((alternatingMapLinearEquiv f).compAlternatingMap (ιMulti R n)) m
-- Mathlib/Data/Int/Log.lean
theorem neg_log_inv_eq_clog (b : ℕ) (r : R) : -log b r⁻¹ = clog b r

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
⊢ -log b r⁻¹ = clog b r

Tactic:
rw [log_inv, neg_neg]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/PairingHeap.lean
theorem Heap.WF.deleteMin {s : Heap α} (h : s.WF le)
    (eq : s.deleteMin le = some (a, s')) : s'.WF le

Proof state:
α : Type u_1
le : α → α → Bool
a : α
s' s : Heap α
h : WF le s
eq : Heap.deleteMin le s = some (a, s')
⊢ WF le s'

Tactic:
cases h with cases eq | node h => exact Heap.WF.combine h

Result:
no goals

Proof state:
case node.refl
α : Type u_1
le : α → α → Bool
a : α
c✝ : Heap α
h : NodeWF le a c✝
⊢ WF le (Heap.combine le c✝)

Tactic:
exact Heap.WF.combine h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
@[simp]
lemma posPart_algebraMap (r : ℝ) : (algebraMap ℝ A r)⁺ = algebraMap ℝ A r⁺

Proof state:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : T2Space A
r : ℝ
⊢ cfc (fun x => x⁺) ((algebraMap ℝ A) r) = (algebraMap ℝ A) r⁺

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : T2Space A
r : ℝ
⊢ ((algebraMap ℝ A) r)⁺ = (algebraMap ℝ A) r⁺

Tactic:
rw [CFC.posPart_def, cfcₙ_eq_cfc]

Result:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : T2Space A
r : ℝ
⊢ cfc (fun x => x⁺) ((algebraMap ℝ A) r) = (algebraMap ℝ A) r⁺
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
protected lemma le_of_add_le_add_right [LE α] [AddRightReflectLE α] (hz : z ≠ ⊥) :
    x + z ≤ y + z → x ≤ y

Proof state:
case intro
α : Type u
inst✝² : Add α
x y : WithBot α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z : α
⊢ x + ↑z ≤ y + ↑z → x ≤ y

Tactic:
cases x <;> cases y <;> simp [← coe_add]

Result:
case intro.coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z a✝¹ a✝ : α
⊢ a✝¹ + z ≤ a✝ + z → a✝¹ ≤ a✝

Proof state:
case intro.coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z a✝¹ a✝ : α
⊢ a✝¹ + z ≤ a✝ + z → a✝¹ ≤ a✝

Tactic:
simpa using le_of_add_le_add_right

Result:
no goals

Proof state:
α : Type u
inst✝² : Add α
x y z : WithBot α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
hz : z ≠ ⊥
⊢ x + z ≤ y + z → x ≤ y

Tactic:
lift z to α using hz

Result:
case intro
α : Type u
inst✝² : Add α
x y : WithBot α
inst✝¹ : LE α
inst✝ : AddRightReflectLE α
z : α
⊢ x + ↑z ≤ y + ↑z → x ≤ y
-- Mathlib/Algebra/Order/Monoid/Unbundled/MinMax.lean
theorem mul_lt_mul_iff_of_le_of_le [MulLeftMono α]
    [MulRightMono α] [MulLeftStrictMono α]
    [MulRightStrictMono α] {a₁ a₂ b₁ b₂ : α} (ha : a₁ ≤ a₂)
    (hb : b₁ ≤ b₂) : a₁ * b₁ < a₂ * b₂ ↔ a₁ < a₂ ∨ b₁ < b₂

Proof state:
case inr
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : MulLeftMono α
inst✝² : MulRightMono α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
hb' : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
exact mul_lt_mul_of_le_of_lt ha hb'

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : MulLeftMono α
inst✝² : MulRightMono α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
ha' : a₁ < a₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
exact mul_lt_mul_of_lt_of_le ha' hb

Result:
no goals

Proof state:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : MulLeftMono α
inst✝² : MulRightMono α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ a₁ * b₁ < a₂ * b₂ ↔ a₁ < a₂ ∨ b₁ < b₂

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

Result:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : MulLeftMono α
inst✝² : MulRightMono α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h : a₁ < a₂ ∨ b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂

Proof state:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : MulLeftMono α
inst✝² : MulRightMono α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h : a₁ < a₂ ∨ b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂

Tactic:
rcases h with ha' | hb'

Result:
case inl
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : MulLeftMono α
inst✝² : MulRightMono α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
ha' : a₁ < a₂
⊢ a₁ * b₁ < a₂ * b₂

case inr
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : MulLeftMono α
inst✝² : MulRightMono α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
hb' : b₁ < b₂
⊢ a₁ * b₁ < a₂ * b₂