harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem affineCombination_affineCombinationSingleWeights [DecidableEq ι] (p : ι → P) {i : ι}
    (hi : i ∈ s) : s.affineCombination k p (affineCombinationSingleWeights k i) = p i

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
p : ι → P
i : ι
hi : i ∈ s
⊢ affineCombinationSingleWeights k i i = 1

Tactic:
simp

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
p : ι → P
i : ι
hi : i ∈ s
⊢ ∀ i2 ∈ s, i2 ≠ i → affineCombinationSingleWeights k i i2 = 0

Tactic:
rintro j - hj

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
p : ι → P
i : ι
hi : i ∈ s
j : ι
hj : j ≠ i
⊢ affineCombinationSingleWeights k i j = 0

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
p : ι → P
i : ι
hi : i ∈ s
j : ι
hj : j ≠ i
⊢ affineCombinationSingleWeights k i j = 0

Tactic:
simp [hj]

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
p : ι → P
i : ι
hi : i ∈ s
⊢ (affineCombination k s p) (affineCombinationSingleWeights k i) = p i

Tactic:
refine s.affineCombination_of_eq_one_of_eq_zero _ _ hi (by simp) ?_

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
p : ι → P
i : ι
hi : i ∈ s
⊢ ∀ i2 ∈ s, i2 ≠ i → affineCombinationSingleWeights k i i2 = 0
-- Mathlib/Analysis/InnerProductSpace/LaxMilgram.lean
theorem ker_eq_bot (coercive : IsCoercive B) : ker B♯ = ⊥

Proof state:
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
w✝ : ℝ≥0
left✝ : 0 < w✝
antilipschitz : AntilipschitzWith w✝ ⇑(continuousLinearMapOfBilin B)
⊢ Function.Injective ⇑(continuousLinearMapOfBilin B)

Tactic:
exact antilipschitz.injective

Result:
no goals

Proof state:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ ker (continuousLinearMapOfBilin B) = ⊥

Tactic:
rw [LinearMapClass.ker_eq_bot]

Result:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ Function.Injective ⇑(continuousLinearMapOfBilin B)

Proof state:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ Function.Injective ⇑(continuousLinearMapOfBilin B)

Tactic:
rcases coercive.antilipschitz with ⟨_, _, antilipschitz⟩

Result:
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
w✝ : ℝ≥0
left✝ : 0 < w✝
antilipschitz : AntilipschitzWith w✝ ⇑(continuousLinearMapOfBilin B)
⊢ Function.Injective ⇑(continuousLinearMapOfBilin B)
-- Mathlib/Algebra/MvPolynomial/Basic.lean
@[simp]
lemma one_coeffsIn : 1 ∈ coeffsIn σ M ↔ 1 ∈ M

Proof state:
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
⊢ 1 ∈ coeffsIn σ M ↔ 1 ∈ M

Tactic:
simpa using C_mem_coeffsIn (x := (1 : S))

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem mem_pmem {a : α} (h : ∀ a ∈ x, p a) (ha : a ∈ x) : f a (h a ha) ∈ pmap f x h

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
x : Option α
a : α
h : ∀ (a : α), a ∈ x → p a
ha✝ : a ∈ x
ha : x = some a
⊢ pmap f x h = some (f a ⋯)

Tactic:
subst ha

Result:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
a : α
h : ∀ (a_1 : α), a_1 ∈ some a → p a_1
ha : a ∈ some a
⊢ pmap f (some a) h = some (f a ⋯)

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
x : Option α
a : α
h : ∀ (a : α), a ∈ x → p a
ha : a ∈ x
⊢ f a ⋯ ∈ pmap f x h

Tactic:
rw [mem_def] at ha ⊢

Result:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
x : Option α
a : α
h : ∀ (a : α), a ∈ x → p a
ha✝ : a ∈ x
ha : x = some a
⊢ pmap f x h = some (f a ⋯)

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
a : α
h : ∀ (a_1 : α), a_1 ∈ some a → p a_1
ha : a ∈ some a
⊢ pmap f (some a) h = some (f a ⋯)

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_pi_le_diam_pow (s : Set (ι → ℝ)) : volume s ≤ EMetric.diam s ^ Fintype.card ι :=
  calc
    volume s ≤ ∏ i : ι, EMetric.diam (Function.eval i '' s) := volume_pi_le_prod_diam s
    _ ≤ ∏ _i : ι, (1 : ℝ≥0) * EMetric.diam s :=
      (Finset.prod_le_prod' fun i _ => (LipschitzWith.eval i).ediam_image_le s)
    _ = EMetric.diam s ^ Fintype.card ι

Proof state:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
⊢ ∏ _i : ι, ↑1 * EMetric.diam s = EMetric.diam s ^ Fintype.card ι

Tactic:
simp only [ENNReal.coe_one, one_mul, Finset.prod_const, Fintype.card]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
lemma count_D_lt_count_U_of_lt_firstReturn {i : ℕ} (hi : i < p.firstReturn) :
    (p.toList.take (i + 1)).count D < (p.toList.take (i + 1)).count U

Proof state:
p : DyckWord
i : ℕ
hi : i < p.firstReturn
ne :
  decide (count U (List.take ((range (↑p).length)[i] + 1) ↑p) = count D (List.take ((range (↑p).length)[i] + 1) ↑p)) =
    false
⊢ count D (List.take (i + 1) ↑p) < count U (List.take (i + 1) ↑p)

Tactic:
rw [decide_eq_false_iff_not, ← ne_eq, getElem_range] at ne

Result:
p : DyckWord
i : ℕ
hi : i < p.firstReturn
ne : count U (List.take (i + 1) ↑p) ≠ count D (List.take (i + 1) ↑p)
⊢ count D (List.take (i + 1) ↑p) < count U (List.take (i + 1) ↑p)

Proof state:
p : DyckWord
i : ℕ
hi : i < p.firstReturn
⊢ count D (List.take (i + 1) ↑p) < count U (List.take (i + 1) ↑p)

Tactic:
have ne := not_of_lt_findIdx hi

Result:
p : DyckWord
i : ℕ
hi : i < p.firstReturn
ne :
  decide (count U (List.take ((range (↑p).length)[i] + 1) ↑p) = count D (List.take ((range (↑p).length)[i] + 1) ↑p)) =
    false
⊢ count D (List.take (i + 1) ↑p) < count U (List.take (i + 1) ↑p)

Proof state:
p : DyckWord
i : ℕ
hi : i < p.firstReturn
ne : count U (List.take (i + 1) ↑p) ≠ count D (List.take (i + 1) ↑p)
⊢ count D (List.take (i + 1) ↑p) < count U (List.take (i + 1) ↑p)

Tactic:
exact lt_of_le_of_ne (p.count_D_le_count_U (i + 1)) ne.symm

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
@[simp]
lemma ofReal_lt_one {p : ℝ} : ENNReal.ofReal p < 1 ↔ p < 1

Proof state:
p : ℝ
⊢ ENNReal.ofReal p < 1 ↔ p < 1

Tactic:
exact mod_cast ofReal_lt_natCast one_ne_zero

Result:
no goals
-- Mathlib/Algebra/Group/Semiconj/Units.lean
theorem units_inv_right {a : M} {x y : Mˣ} (h : SemiconjBy a x y) : SemiconjBy a ↑x⁻¹ ↑y⁻¹ :=
  calc
    a * ↑x⁻¹ = ↑y⁻¹ * (y * a) * ↑x⁻¹

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
⊢ a * ↑x⁻¹ = ↑y⁻¹ * (↑y * a) * ↑x⁻¹

Tactic:
rw [Units.inv_mul_cancel_left]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
⊢ ↑y⁻¹ * (↑y * a) * ↑x⁻¹ = ↑y⁻¹ * a

Tactic:
rw [← h.eq, mul_assoc, Units.mul_inv_cancel_right]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_sq_le_one : sin x ^ 2 ≤ 1

Proof state:
x : ℝ
⊢ sin x ^ 2 ≤ 1

Tactic:
rw [← sin_sq_add_cos_sq x]

Result:
x : ℝ
⊢ sin x ^ 2 ≤ sin x ^ 2 + cos x ^ 2

Proof state:
x : ℝ
⊢ sin x ^ 2 ≤ sin x ^ 2 + cos x ^ 2

Tactic:
exact le_add_of_nonneg_right (sq_nonneg _)

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem div_ne_zero (ha : a ≠ 0) (hb : b ≠ 0) : a / b ≠ 0

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
ha : a ≠ 0
hb : b ≠ 0
⊢ a / b ≠ 0

Tactic:
rw [div_eq_mul_inv]

Result:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b⁻¹ ≠ 0

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b⁻¹ ≠ 0

Tactic:
exact mul_ne_zero ha (inv_ne_zero hb)

Result:
no goals
-- Mathlib/CategoryTheory/EffectiveEpi/Comp.lean
theorem effectiveEpiFamilyStructCompIso_aux
    {W : C} (e : (a : α) → X a ⟶ W)
    (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
      g₁ ≫ π a₁ ≫ i = g₂ ≫ π a₂ ≫ i → g₁ ≫ e a₁ = g₂ ≫ e a₂)
    {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂) (hg : g₁ ≫ π a₁ = g₂ ≫ π a₂) :
    g₁ ≫ e a₁ = g₂ ≫ e a₂

Proof state:
case a
C : Type u_1
inst✝ : Category.{u_3, u_1} C
B B' : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
i : B ⟶ B'
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ ≫ i = g₂ ≫ π a₂ ≫ i → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ (g₂ ≫ π a₂) ≫ i = g₂ ≫ π a₂ ≫ i

Tactic:
simp

Result:
no goals

Proof state:
case a
C : Type u_1
inst✝ : Category.{u_3, u_1} C
B B' : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
i : B ⟶ B'
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ ≫ i = g₂ ≫ π a₂ ≫ i → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ g₁ ≫ π a₁ ≫ i = g₂ ≫ π a₂ ≫ i

Tactic:
rw [← Category.assoc, hg]

Result:
case a
C : Type u_1
inst✝ : Category.{u_3, u_1} C
B B' : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
i : B ⟶ B'
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ ≫ i = g₂ ≫ π a₂ ≫ i → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ (g₂ ≫ π a₂) ≫ i = g₂ ≫ π a₂ ≫ i

Proof state:
C : Type u_1
inst✝ : Category.{u_3, u_1} C
B B' : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
i : B ⟶ B'
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ ≫ i = g₂ ≫ π a₂ ≫ i → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ g₁ ≫ e a₁ = g₂ ≫ e a₂

Tactic:
apply h

Result:
case a
C : Type u_1
inst✝ : Category.{u_3, u_1} C
B B' : C
α : Type u_2
X : α → C
π : (a : α) → X a ⟶ B
i : B ⟶ B'
W : C
e : (a : α) → X a ⟶ W
h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ ≫ i = g₂ ≫ π a₂ ≫ i → g₁ ≫ e a₁ = g₂ ≫ e a₂
Z : C
a₁ a₂ : α
g₁ : Z ⟶ X a₁
g₂ : Z ⟶ X a₂
hg : g₁ ≫ π a₁ = g₂ ≫ π a₂
⊢ g₁ ≫ π a₁ ≫ i = g₂ ≫ π a₂ ≫ i
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_σ_self' {n} {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = Fin.castSucc i) :
    X.δ j ≫ X.σ i = 𝟙 _

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.castSucc
⊢ X.δ j ≫ X.σ i = 𝟙 (X ^⦋n⦌)

Tactic:
subst H

Result:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.δ i.castSucc ≫ X.σ i = 𝟙 (X ^⦋n⦌)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.δ i.castSucc ≫ X.σ i = 𝟙 (X ^⦋n⦌)

Tactic:
rw [δ_comp_σ_self]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Prod.lean
theorem lintegral_prod_deterministic {f : α → γ} (hf : Measurable f) (κ : Kernel α β)
    [IsSFiniteKernel κ] (a : α) {g : (β × γ) → ℝ≥0∞} (hg : Measurable g) :
    ∫⁻ p, g p ∂(κ ×ₖ (deterministic f hf)) a = ∫⁻ b, g (b, f a) ∂κ a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → γ
hf : Measurable f
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (p : β × γ), g p ∂(κ ×ₖ deterministic f hf) a = ∫⁻ (b : β), g (b, f a) ∂κ a

Tactic:
rw [lintegral_prod_symm _ _ _ hg, lintegral_deterministic' _ hg.lintegral_prod_left']

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem exists_right_inv_of_exists_left_inv {α} [MonoidWithZero α]
    (h : ∀ a : α, a ≠ 0 → ∃ b : α, b * a = 1) {a : α} (ha : a ≠ 0) : ∃ b : α, a * b = 1

Proof state:
case inr.intro
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
⊢ ∃ b, a * b = 1

Tactic:
obtain ⟨c, hc⟩ := h b (left_ne_zero_of_mul <| hb.trans_ne one_ne_zero)

Result:
case inr.intro.intro
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
⊢ ∃ b, a * b = 1

Proof state:
case inl
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Subsingleton α
⊢ ∃ b, a * b = 1

Tactic:
exact ⟨a, Subsingleton.elim _ _⟩

Result:
no goals

Proof state:
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
⊢ ∃ b, a * b = 1

Tactic:
obtain _ | _ := subsingleton_or_nontrivial α

Result:
case inl
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Subsingleton α
⊢ ∃ b, a * b = 1

case inr
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
⊢ ∃ b, a * b = 1

Proof state:
case inr.intro.intro
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
⊢ ∃ b, a * b = 1

Tactic:
refine ⟨b, ?_⟩

Result:
case inr.intro.intro
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
⊢ a * b = 1

Proof state:
case inr
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
⊢ ∃ b, a * b = 1

Tactic:
obtain ⟨b, hb⟩ := h a ha

Result:
case inr.intro
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
⊢ ∃ b, a * b = 1

Proof state:
case inr.intro.intro
α : Type u_3
inst✝ : MonoidWithZero α
h : ∀ (a : α), a ≠ 0 → ∃ b, b * a = 1
a : α
ha : a ≠ 0
h✝ : Nontrivial α
b : α
hb : b * a = 1
c : α
hc : c * b = 1
⊢ a * b = 1

Tactic:
conv_lhs => rw [← one_mul (a * b), ← hc, mul_assoc, ← mul_assoc b, hb, one_mul, hc]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
lemma abs_le_iff_mul_self_le : |a| ≤ |b| ↔ a * a ≤ b * b

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ |a| ≤ |b| ↔ a * a ≤ b * b

Tactic:
rw [← abs_mul_abs_self, ← abs_mul_abs_self b]

Result:
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ |a| ≤ |b| ↔ |a| * |a| ≤ |b| * |b|

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ |a| ≤ |b| ↔ |a| * |a| ≤ |b| * |b|

Tactic:
exact mul_self_le_mul_self_iff (abs_nonneg a) (abs_nonneg b)

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Limits/Products.lean
theorem isEmbedding_prodMap {W X Y Z : TopCat.{u}} {f : W ⟶ X} {g : Y ⟶ Z} (hf : IsEmbedding f)
    (hg : IsEmbedding g) : IsEmbedding (Limits.prod.map f g) :=
  ⟨isInducing_prodMap hf.isInducing hg.isInducing, by
    haveI := (TopCat.mono_iff_injective _).mpr hf.injective
    haveI := (TopCat.mono_iff_injective _).mpr hg.injective
    exact (TopCat.mono_iff_injective _).mp inferInstance⟩

Proof state:
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : IsEmbedding ⇑(ConcreteCategory.hom f)
hg : IsEmbedding ⇑(ConcreteCategory.hom g)
this : Mono f
⊢ Function.Injective ⇑(ConcreteCategory.hom (prod.map f g))

Tactic:
haveI := (TopCat.mono_iff_injective _).mpr hg.injective

Result:
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : IsEmbedding ⇑(ConcreteCategory.hom f)
hg : IsEmbedding ⇑(ConcreteCategory.hom g)
this✝ : Mono f
this : Mono g
⊢ Function.Injective ⇑(ConcreteCategory.hom (prod.map f g))

Proof state:
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : IsEmbedding ⇑(ConcreteCategory.hom f)
hg : IsEmbedding ⇑(ConcreteCategory.hom g)
⊢ Function.Injective ⇑(ConcreteCategory.hom (prod.map f g))

Tactic:
haveI := (TopCat.mono_iff_injective _).mpr hf.injective

Result:
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : IsEmbedding ⇑(ConcreteCategory.hom f)
hg : IsEmbedding ⇑(ConcreteCategory.hom g)
this : Mono f
⊢ Function.Injective ⇑(ConcreteCategory.hom (prod.map f g))

Proof state:
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf : IsEmbedding ⇑(ConcreteCategory.hom f)
hg : IsEmbedding ⇑(ConcreteCategory.hom g)
this✝ : Mono f
this : Mono g
⊢ Function.Injective ⇑(ConcreteCategory.hom (prod.map f g))

Tactic:
exact (TopCat.mono_iff_injective _).mp inferInstance

Result:
no goals
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem quotMapOfEquivQuotMapCMapSpanMk_symm_mk (x : AdjoinRoot f) :
    (quotMapOfEquivQuotMapCMapSpanMk I f).symm
        (Ideal.Quotient.mk ((I.map (C : R →+* R[X])).map (Ideal.Quotient.mk (span {f}))) x) =
      Ideal.Quotient.mk (I.map (of f)) x

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
f : R[X]
x : AdjoinRoot f
⊢ (quotMapOfEquivQuotMapCMapSpanMk I f).symm
      ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))) x) =
    (Ideal.Quotient.mk (Ideal.map (of f) I)) x

Tactic:
rw [quotMapOfEquivQuotMapCMapSpanMk, Ideal.quotEquivOfEq_symm]

Result:
R : Type u
inst✝ : CommRing R
I : Ideal R
f : R[X]
x : AdjoinRoot f
⊢ (quotEquivOfEq ⋯) ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))) x) =
    (Ideal.Quotient.mk (Ideal.map (of f) I)) x

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
f : R[X]
x : AdjoinRoot f
⊢ (quotEquivOfEq ⋯) ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (span {f})) (Ideal.map C I))) x) =
    (Ideal.Quotient.mk (Ideal.map (of f) I)) x

Tactic:
exact Ideal.quotEquivOfEq_mk _ _

Result:
no goals
-- Mathlib/Analysis/Complex/Isometry.lean
theorem LinearIsometry.re_apply_eq_re {f : ℂ →ₗᵢ[ℝ] ℂ} (h : f 1 = 1) (z : ℂ) : (f z).re = z.re

Proof state:
f : ℂ →ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
⊢ (f z).re = z.re

Tactic:
apply LinearIsometry.re_apply_eq_re_of_add_conj_eq

Result:
case h₃
f : ℂ →ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
⊢ ∀ (z : ℂ), z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)

Proof state:
case h₃
f : ℂ →ₗᵢ[ℝ] ℂ
h : f 1 = 1
z : ℂ
⊢ ∀ (z : ℂ), z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)

Tactic:
intro z

Result:
case h₃
f : ℂ →ₗᵢ[ℝ] ℂ
h : f 1 = 1
z✝ z : ℂ
⊢ z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)

Proof state:
case h₃
f : ℂ →ₗᵢ[ℝ] ℂ
h : f 1 = 1
z✝ z : ℂ
⊢ z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)

Tactic:
apply LinearIsometry.im_apply_eq_im h

Result:
no goals
-- Mathlib/Data/List/Map2.lean
theorem map₂Left'_nil_right (f : α → Option β → γ) (as) :
    map₂Left' f as [] = (as.map fun a => f a none, [])

Proof state:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
as : List α
⊢ map₂Left' f as [] = (map (fun a => f a none) as, [])

Tactic:
cases as <;> rfl

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem snd_of_isColimit {X Y : C} {t : BinaryBicone X Y} (ht : IsColimit t.toCocone) :
    t.snd = ht.desc (BinaryCofan.mk 0 (𝟙 Y))

Proof state:
case x
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsColimit t.toCocone
⊢ ∀ (j : Discrete WalkingPair), t.toCocone.ι.app j ≫ t.snd = (BinaryCofan.mk 0 (𝟙 Y)).ι.app j

Tactic:
rintro ⟨⟨⟩⟩ <;> dsimp <;> simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsColimit t.toCocone
⊢ t.snd = ht.desc (BinaryCofan.mk 0 (𝟙 Y))

Tactic:
apply ht.uniq (BinaryCofan.mk 0 (𝟙 Y))

Result:
case x
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsColimit t.toCocone
⊢ ∀ (j : Discrete WalkingPair), t.toCocone.ι.app j ≫ t.snd = (BinaryCofan.mk 0 (𝟙 Y)).ι.app j
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_empty : gauge (∅ : Set E) = 0

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
⊢ gauge ∅ = 0

Tactic:
ext

Result:
case h
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
x✝ : E
⊢ gauge ∅ x✝ = 0 x✝

Proof state:
case h
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
x✝ : E
⊢ gauge ∅ x✝ = 0 x✝

Tactic:
simp only [gauge_def', Real.sInf_empty, mem_empty_iff_false, Pi.zero_apply, sep_false]

Result:
no goals
-- Mathlib/Dynamics/Ergodic/MeasurePreserving.lean
theorem symm (e : α ≃ᵐ β) {μa : Measure α} {μb : Measure β} (h : MeasurePreserving e μa μb) :
    MeasurePreserving e.symm μb μa :=
  ⟨e.symm.measurable, by
    rw [← h.map_eq, map_map e.symm.measurable e.measurable, e.symm_comp_self, map_id]⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
μa : Measure α
μb : Measure β
h : MeasurePreserving (⇑e) μa μb
⊢ map (⇑e.symm) μb = μa

Tactic:
rw [← h.map_eq, map_map e.symm.measurable e.measurable, e.symm_comp_self, map_id]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
theorem polynomial_relation (P : Fin 3 → R) : 3 * eval P W'.polynomial =
    P x * eval P W'.polynomialX + P y * eval P W'.polynomialY + P z * eval P W'.polynomialZ

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ 3 *
      (P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
        (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3)) =
    P x * (W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2)) +
        P y * (2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2) +
      P z *
        (P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2))

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ 3 * (eval P) W'.polynomial =
    P x * (eval P) W'.polynomialX + P y * (eval P) W'.polynomialY + P z * (eval P) W'.polynomialZ

Tactic:
rw [eval_polynomial, eval_polynomialX, eval_polynomialY, eval_polynomialZ]

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ 3 *
      (P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
        (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3)) =
    P x * (W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * P z ^ 2)) +
        P y * (2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * P z ^ 2) +
      P z *
        (P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2))