harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/GroupAction/ConjAct.lean
theorem _root_.MulAut.conjNormal_symm_apply {H : Subgroup G} [H.Normal] (g : G) (h : H) :
    ↑((MulAut.conjNormal g).symm h) = g⁻¹ * h * g

Proof state:
G : Type u_3
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
h : ↥H
⊢ ofConjAct (toConjAct.toMonoidHom g)⁻¹ * ↑h * (toConjAct.toMonoidHom g)⁻¹⁻¹ = g⁻¹ * ↑h * g

Tactic:
rw [inv_inv]

Result:
G : Type u_3
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
h : ↥H
⊢ ofConjAct (toConjAct.toMonoidHom g)⁻¹ * ↑h * toConjAct.toMonoidHom g = g⁻¹ * ↑h * g

Proof state:
G : Type u_3
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
h : ↥H
⊢ ↑((MulEquiv.symm (MulAut.conjNormal g)) h) = g⁻¹ * ↑h * g

Tactic:
change _ * _⁻¹⁻¹ = _

Result:
G : Type u_3
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
h : ↥H
⊢ ofConjAct (toConjAct.toMonoidHom g)⁻¹ * ↑h * (toConjAct.toMonoidHom g)⁻¹⁻¹ = g⁻¹ * ↑h * g

Proof state:
G : Type u_3
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
h : ↥H
⊢ ofConjAct (toConjAct.toMonoidHom g)⁻¹ * ↑h * toConjAct.toMonoidHom g = g⁻¹ * ↑h * g

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
@[simp, nolint simpNF] protected lemma pow_eq_zero {a : ℕ} : ∀ {n : ℕ}, a ^ n = 0 ↔ a = 0 ∧ n ≠ 0
  | 0 => by simp
  | n + 1 => by rw [Nat.pow_succ, mul_eq_zero, Nat.pow_eq_zero]; omega

Proof state:
a n : ℕ
⊢ a ^ (n + 1) = 0 ↔ a = 0 ∧ n + 1 ≠ 0

Tactic:
rw [Nat.pow_succ, mul_eq_zero, Nat.pow_eq_zero]

Result:
a n : ℕ
⊢ a = 0 ∧ n ≠ 0 ∨ a = 0 ↔ a = 0 ∧ n + 1 ≠ 0

Proof state:
a : ℕ
⊢ a ^ 0 = 0 ↔ a = 0 ∧ 0 ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
a n : ℕ
⊢ a = 0 ∧ n ≠ 0 ∨ a = 0 ↔ a = 0 ∧ n + 1 ≠ 0

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem toFinsupp_mul (a b : R[X]) : (a * b).toFinsupp = a.toFinsupp * b.toFinsupp

Proof state:
case ofFinsupp
R : Type u
inst✝ : Semiring R
b : R[X]
toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝ } * b).toFinsupp = { toFinsupp := toFinsupp✝ }.toFinsupp * b.toFinsupp

Tactic:
cases b

Result:
case ofFinsupp.ofFinsupp
R : Type u
inst✝ : Semiring R
toFinsupp✝¹ toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝¹ } * { toFinsupp := toFinsupp✝ }).toFinsupp =
    { toFinsupp := toFinsupp✝¹ }.toFinsupp * { toFinsupp := toFinsupp✝ }.toFinsupp

Proof state:
case ofFinsupp.ofFinsupp
R : Type u
inst✝ : Semiring R
toFinsupp✝¹ toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝¹ } * { toFinsupp := toFinsupp✝ }).toFinsupp =
    { toFinsupp := toFinsupp✝¹ }.toFinsupp * { toFinsupp := toFinsupp✝ }.toFinsupp

Tactic:
rw [← ofFinsupp_mul]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
a b : R[X]
⊢ (a * b).toFinsupp = a.toFinsupp * b.toFinsupp

Tactic:
cases a

Result:
case ofFinsupp
R : Type u
inst✝ : Semiring R
b : R[X]
toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝ } * b).toFinsupp = { toFinsupp := toFinsupp✝ }.toFinsupp * b.toFinsupp
-- Mathlib/Data/Bool/Basic.lean
theorem not_iff_not : ∀ {b : Bool}, !b ↔ ¬b

Proof state:
⊢ ∀ {b : Bool}, (!b) = true ↔ ¬b = true

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Basic.lean
theorem lift_of (F : G →* A) (x) : lift k G A F (of k G x) = F x

Proof state:
k : Type u₁
G : Type u₂
inst✝³ : CommSemiring k
inst✝² : Monoid G
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra k A
F : G →* A
x : G
⊢ ((lift k G A) F) ((of k G) x) = F x

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean
theorem zmod_char_primitive_of_eq_one_only_at_zero (n : ℕ) (ψ : AddChar (ZMod n) C)
    (hψ : ∀ a, ψ a = 1 → a = 0) : IsPrimitive ψ

Proof state:
C : Type v
inst✝ : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ψ a = 1 → a = 0
a : ZMod n
ha : a ≠ 0
hf : ψ.mulShift a = 1
⊢ False

Tactic:
have h : mulShift ψ a 1 = (1 : AddChar (ZMod n) C) (1 : ZMod n) :=
  congr_fun (congr_arg (↑) hf) 1

Result:
C : Type v
inst✝ : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ψ a = 1 → a = 0
a : ZMod n
ha : a ≠ 0
hf : ψ.mulShift a = 1
h : (ψ.mulShift a) 1 = 1 1
⊢ False

Proof state:
C : Type v
inst✝ : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ψ a = 1 → a = 0
a : ZMod n
ha : a ≠ 0
hf : ψ.mulShift a = 1
h : (ψ.mulShift a) 1 = 1 1
⊢ False

Tactic:
rw [mulShift_apply, mul_one] at h

Result:
C : Type v
inst✝ : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ψ a = 1 → a = 0
a : ZMod n
ha : a ≠ 0
hf : ψ.mulShift a = 1
h : ψ a = 1 1
⊢ False

Proof state:
C : Type v
inst✝ : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ψ a = 1 → a = 0
a : ZMod n
ha : a ≠ 0
hf : ψ.mulShift a = 1
h : ψ a = 1 1
⊢ False

Tactic:
exact ha (hψ a h)

Result:
no goals

Proof state:
C : Type v
inst✝ : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ψ a = 1 → a = 0
⊢ ψ.IsPrimitive

Tactic:
refine fun a ha hf => ?_

Result:
C : Type v
inst✝ : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), ψ a = 1 → a = 0
a : ZMod n
ha : a ≠ 0
hf : ψ.mulShift a = 1
⊢ False
-- Mathlib/Probability/Independence/Kernel.lean
@[simp] lemma iIndepSet_zero_right : iIndepSet s κ 0

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
s : ι → Set Ω
⊢ iIndepSet s κ 0

Tactic:
simp [iIndepSet]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `le_div_iff₀` for a version with multiplication on the other side. -/
lemma le_div_iff₀' (hc : 0 < c) : a ≤ b / c ↔ c * a ≤ b

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulMono G₀
a b c : G₀
hc : 0 < c
this : MulPosMono G₀
⊢ a ≤ b / c ↔ c * a ≤ b

Tactic:
rw [le_div_iff₀ hc, mul_comm]

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulMono G₀
a b c : G₀
hc : 0 < c
⊢ a ≤ b / c ↔ c * a ≤ b

Tactic:
have := posMulMono_iff_mulPosMono.1 ‹_›

Result:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulMono G₀
a b c : G₀
hc : 0 < c
this : MulPosMono G₀
⊢ a ≤ b / c ↔ c * a ≤ b
-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem LocallyIntegrable.aestronglyMeasurable [SecondCountableTopology X]
    (hf : LocallyIntegrable f μ) : AEStronglyMeasurable f μ

Proof state:
X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝ : SecondCountableTopology X
hf : LocallyIntegrable f μ
⊢ AEStronglyMeasurable f μ

Tactic:
simpa only [restrict_univ] using (locallyIntegrableOn_univ.mpr hf).aestronglyMeasurable

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Defs.lean
/-- The linear map version of `Function.Injective.comp_left` -/
lemma _root_.Function.Injective.injective_linearMapComp_left (hf : Injective f) :
    Injective fun g : M₁ →ₛₗ[σ₁₂] M₂ ↦ f.comp g :=
  fun g₁ g₂ (h : f.comp g₁ = f.comp g₂) ↦ ext fun x ↦ hf <| by rw [← comp_apply, h, comp_apply]

Proof state:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst✝⁶ : Semiring R₁
inst✝⁵ : Semiring R₂
inst✝⁴ : Semiring R₃
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
hf : Injective ⇑f
g₁ g₂ : M₁ →ₛₗ[σ₁₂] M₂
h : f.comp g₁ = f.comp g₂
x : M₁
⊢ f (g₁ x) = f (g₂ x)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem cos_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : Real.Angle.cos (o.oangle x (x + y)) * ‖x + y‖ = ‖x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle x (x + y)).sign = 1

Tactic:
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ (o.oangle x (x + y)).cos * ‖x + y‖ = ‖x‖

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
  InnerProductGeometry.cos_angle_add_mul_norm_of_inner_eq_zero
    (o.inner_eq_zero_of_oangle_eq_pi_div_two h)]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle x (x + y)).cos * ‖x + y‖ = ‖x‖

Tactic:
have hs : (o.oangle x (x + y)).sign = 1 := by
  rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ (o.oangle x (x + y)).cos * ‖x + y‖ = ‖x‖
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem le_length_eraseP (l : List α) : l.length - 1 ≤ (l.eraseP p).length

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ l.length - 1 ≤ (eraseP p l).length

Tactic:
rw [length_eraseP]

Result:
α : Type u_1
p : α → Bool
l : List α
⊢ l.length - 1 ≤ if l.any p = true then l.length - 1 else l.length

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ l.length - 1 ≤ if l.any p = true then l.length - 1 else l.length

Tactic:
split <;> simp

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioc_diff_Ioo_same (h : a < b) : Ioc a b \ Ioo a b = {b}

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a < b
⊢ Ioc a b \ Ioo a b = {b}

Tactic:
rw [← Ioc_diff_right, diff_diff_cancel_left (singleton_subset_iff.2 <| right_mem_Ioc.2 h)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem filterMap_attachWith {q : α → Prop} {l : List α} {f : {x // q x} → Option β} (H) :
    (l.attachWith q H).filterMap f = l.attach.filterMap (fun ⟨x, h⟩ => f ⟨x, H _ h⟩)

Proof state:
case cons
α : Type u_1
β : Type u_2
q : α → Prop
f : { x // q x } → Option β
x : α
xs : List α
ih :
  ∀ (H : ∀ (x : α), x ∈ xs → q x),
    filterMap f (xs.attachWith q H) =
      filterMap
        (fun x =>
          match x with
          | ⟨x, h⟩ => f ⟨x, ⋯⟩)
        xs.attach
H : ∀ (x_1 : α), x_1 ∈ x :: xs → q x_1
⊢ filterMap f ((x :: xs).attachWith q H) =
    filterMap
      (fun x_1 =>
        match x_1 with
        | ⟨x_2, h⟩ => f ⟨x_2, ⋯⟩)
      (x :: xs).attach

Tactic:
simp only [attachWith_cons, filterMap_cons]

Result:
case cons
α : Type u_1
β : Type u_2
q : α → Prop
f : { x // q x } → Option β
x : α
xs : List α
ih :
  ∀ (H : ∀ (x : α), x ∈ xs → q x),
    filterMap f (xs.attachWith q H) =
      filterMap
        (fun x =>
          match x with
          | ⟨x, h⟩ => f ⟨x, ⋯⟩)
        xs.attach
H : ∀ (x_1 : α), x_1 ∈ x :: xs → q x_1
⊢ (match f ⟨x, ⋯⟩ with
    | none => filterMap f (xs.attachWith q ⋯)
    | some b => b :: filterMap f (xs.attachWith q ⋯)) =
    filterMap (fun x_1 => f ⟨x_1.val, ⋯⟩) (x :: xs).attach

Proof state:
α : Type u_1
β : Type u_2
q : α → Prop
l : List α
f : { x // q x } → Option β
H : ∀ (x : α), x ∈ l → q x
⊢ filterMap f (l.attachWith q H) =
    filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => f ⟨x, ⋯⟩)
      l.attach

Tactic:
induction l with
| nil => rfl
| cons x xs ih =>
  simp only [attachWith_cons, filterMap_cons]
  split <;> simp_all [Function.comp_def]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
q : α → Prop
f : { x // q x } → Option β
H : ∀ (x : α), x ∈ [] → q x
⊢ filterMap f ([].attachWith q H) =
    filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => f ⟨x, ⋯⟩)
      [].attach

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
q : α → Prop
f : { x // q x } → Option β
x : α
xs : List α
ih :
  ∀ (H : ∀ (x : α), x ∈ xs → q x),
    filterMap f (xs.attachWith q H) =
      filterMap
        (fun x =>
          match x with
          | ⟨x, h⟩ => f ⟨x, ⋯⟩)
        xs.attach
H : ∀ (x_1 : α), x_1 ∈ x :: xs → q x_1
⊢ (match f ⟨x, ⋯⟩ with
    | none => filterMap f (xs.attachWith q ⋯)
    | some b => b :: filterMap f (xs.attachWith q ⋯)) =
    filterMap (fun x_1 => f ⟨x_1.val, ⋯⟩) (x :: xs).attach

Tactic:
split <;> simp_all [Function.comp_def]

Result:
no goals
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem LieIdeal.map_lowerCentralSeries_le (k : ℕ) {f : L →ₗ⁅R⁆ L'} :
    LieIdeal.map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k

Proof state:
case succ
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
k : ℕ
ih : map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k
⊢ map f (lowerCentralSeries R L L (k + 1)) ≤ lowerCentralSeries R L' L' (k + 1)

Tactic:
simp only [LieModule.lowerCentralSeries_succ]

Result:
case succ
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
k : ℕ
ih : map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k
⊢ map f ⁅⊤, lowerCentralSeries R L L k⁆ ≤ ⁅⊤, lowerCentralSeries R L' L' k⁆

Proof state:
case zero
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
⊢ map f (lowerCentralSeries R L L 0) ≤ lowerCentralSeries R L' L' 0

Tactic:
simp only [LieModule.lowerCentralSeries_zero, le_top]

Result:
no goals

Proof state:
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
k : ℕ
f : L →ₗ⁅R⁆ L'
⊢ map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k

Tactic:
induction k with
| zero => simp only [LieModule.lowerCentralSeries_zero, le_top]
| succ k ih =>
  simp only [LieModule.lowerCentralSeries_succ]
  exact le_trans (LieIdeal.map_bracket_le f) (LieSubmodule.mono_lie le_top ih)

Result:
no goals

Proof state:
case succ
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
k : ℕ
ih : map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k
⊢ map f ⁅⊤, lowerCentralSeries R L L k⁆ ≤ ⁅⊤, lowerCentralSeries R L' L' k⁆

Tactic:
exact le_trans (LieIdeal.map_bracket_le f) (LieSubmodule.mono_lie le_top ih)

Result:
no goals
-- Mathlib/RingTheory/Radical.lean
theorem radical_one_eq : radical (1 : M) = 1

Proof state:
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
⊢ radical 1 = 1

Tactic:
rw [radical, primeFactors, normalizedFactors_one, Multiset.toFinset_zero, Finset.prod_empty]

Result:
no goals

Proof state:
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
⊢ radical 1 = 1

Tactic:
classical
rw [radical, primeFactors, normalizedFactors_one, Multiset.toFinset_zero, Finset.prod_empty]

Result:
no goals
-- Mathlib/Tactic/NormNum/Basic.lean
theorem isRat_eq_true [Ring α] : {a b : α} → {n : ℤ} → {d : ℕ} →
    IsRat a n d → IsRat b n d → a = b
  | _, _, _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => by congr; apply Subsingleton.elim

Proof state:
case e_a.h.e_5.h
α : Type u
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
inv✝¹ inv✝ : Invertible ↑denom✝
⊢ inv✝¹ = inv✝

Tactic:
apply Subsingleton.elim

Result:
no goals

Proof state:
α : Type u
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
inv✝¹ inv✝ : Invertible ↑denom✝
⊢ ↑num✝ * ⅟↑denom✝ = ↑num✝ * ⅟↑denom✝

Tactic:
congr

Result:
case e_a.h.e_5.h
α : Type u
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
inv✝¹ inv✝ : Invertible ↑denom✝
⊢ inv✝¹ = inv✝
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem multipliable_of_finite_mulSupport (h : (mulSupport f).Finite) : Multipliable f

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
h : (mulSupport f).Finite
⊢ ∀ b ∉ h.toFinset, f b = 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
h : (mulSupport f).Finite
⊢ Multipliable f

Tactic:
apply multipliable_of_ne_finset_one (s := h.toFinset)

Result:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
h : (mulSupport f).Finite
⊢ ∀ b ∉ h.toFinset, f b = 1
-- Mathlib/NumberTheory/ModularForms/SlashActions.lean
theorem slash_mul (k : ℤ) (A B : GL(2, ℝ)⁺) (f : ℍ → ℂ) :
    f ∣[k] (A * B) = (f ∣[k] A) ∣[k] B

Proof state:
case h
k : ℤ
A B : ↥GL(2, ℝ)⁺
f : ℍ → ℂ
x : ℍ
⊢ (f ∣[k](A * B)) x = ((f ∣[k]A) ∣[k]B) x

Tactic:
simp only [slash, UpperHalfPlane.denom_cocycle A B x]

Result:
case h
k : ℤ
A B : ↥GL(2, ℝ)⁺
f : ℍ → ℂ
x : ℍ
⊢ f ((A * B) • x) * ↑(↑↑(A * B)).det ^ (k - 1) * (denom A (smulAux B x) * denom B x) ^ (-k) =
    f (A • B • x) * ↑(↑↑A).det ^ (k - 1) * denom A (B • x) ^ (-k) * ↑(↑↑B).det ^ (k - 1) * denom B x ^ (-k)

Proof state:
k : ℤ
A B : ↥GL(2, ℝ)⁺
f : ℍ → ℂ
⊢ f ∣[k](A * B) = (f ∣[k]A) ∣[k]B

Tactic:
ext1 x

Result:
case h
k : ℤ
A B : ↥GL(2, ℝ)⁺
f : ℍ → ℂ
x : ℍ
⊢ (f ∣[k](A * B)) x = ((f ∣[k]A) ∣[k]B) x

Proof state:
case h
k : ℤ
A B : ↥GL(2, ℝ)⁺
f : ℍ → ℂ
x : ℍ
⊢ f (A • B • x) * (↑(↑↑A).det * ↑(↑↑B).det) ^ (k - 1) *
      ((↑(↑↑A 1 0) * ((↑(↑↑B 0 0) * ↑x + ↑(↑↑B 0 1)) / (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1))) + ↑(↑↑A 1 1)) *
          (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1))) ^
        (-k) =
    f (A • B • x) * ↑(↑↑A).det ^ (k - 1) *
          (↑(↑↑A 1 0) * ((↑(↑↑B 0 0) * ↑x + ↑(↑↑B 0 1)) / (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1))) + ↑(↑↑A 1 1)) ^ (-k) *
        ↑(↑↑B).det ^ (k - 1) *
      (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1)) ^ (-k)

Tactic:
rw [mul_zpow, mul_right_comm _ _ (((↑ₘ[ℝ] B).det : ℂ) ^ (k - 1)),
  ← mul_assoc, mul_zpow, ← mul_assoc]

Result:
no goals

Proof state:
case h
k : ℤ
A B : ↥GL(2, ℝ)⁺
f : ℍ → ℂ
x : ℍ
⊢ f ((A * B) • x) * ↑(↑↑(A * B)).det ^ (k - 1) * (denom A (smulAux B x) * denom B x) ^ (-k) =
    f (A • B • x) * ↑(↑↑A).det ^ (k - 1) * denom A (B • x) ^ (-k) * ↑(↑↑B).det ^ (k - 1) * denom B x ^ (-k)

Tactic:
simp only [mul_smul, Subgroup.coe_mul, Units.val_mul, Matrix.det_mul, ofReal_mul, denom, smulAux,
  smulAux', num, coe_mk, UpperHalfPlane.coe_smul]

Result:
case h
k : ℤ
A B : ↥GL(2, ℝ)⁺
f : ℍ → ℂ
x : ℍ
⊢ f (A • B • x) * (↑(↑↑A).det * ↑(↑↑B).det) ^ (k - 1) *
      ((↑(↑↑A 1 0) * ((↑(↑↑B 0 0) * ↑x + ↑(↑↑B 0 1)) / (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1))) + ↑(↑↑A 1 1)) *
          (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1))) ^
        (-k) =
    f (A • B • x) * ↑(↑↑A).det ^ (k - 1) *
          (↑(↑↑A 1 0) * ((↑(↑↑B 0 0) * ↑x + ↑(↑↑B 0 1)) / (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1))) + ↑(↑↑A 1 1)) ^ (-k) *
        ↑(↑↑B).det ^ (k - 1) *
      (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1)) ^ (-k)
-- Mathlib/Order/Minimal.lean
theorem minimal_and_iff_left_of_imp (hPQ : ∀ ⦃x⦄, P x → Q x) :
    Minimal (fun x ↦ Q x ∧ P x) x ↔ Q x ∧ (Minimal P x)

Proof state:
α : Type u_1
P Q : α → Prop
x : α
inst✝ : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
⊢ Minimal (fun x => Q x ∧ P x) x ↔ Q x ∧ Minimal P x

Tactic:
simp_rw [iff_comm, and_comm, minimal_and_iff_right_of_imp hPQ, and_comm]

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject.lean
theorem eqToHom_proj {I : Type*} {x x' : GradedObject I C} (h : x = x') (i : I) :
    (eqToHom h : x ⟶ x') i = eqToHom (funext_iff.mp h i)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
I : Type u_1
x : GradedObject I C
i : I
⊢ eqToHom ⋯ i = eqToHom ⋯

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
I : Type u_1
x x' : GradedObject I C
h : x = x'
i : I
⊢ eqToHom h i = eqToHom ⋯

Tactic:
subst h

Result:
C : Type u
inst✝ : Category.{v, u} C
I : Type u_1
x : GradedObject I C
i : I
⊢ eqToHom ⋯ i = eqToHom ⋯
-- Mathlib/Analysis/BoxIntegral/Box/Basic.lean
theorem coe_mk' (l u : ι → ℝ) : (mk' l u : Set (ι → ℝ)) = pi univ fun i ↦ Ioc (l i) (u i)

Proof state:
case neg.intro
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
⊢ ↑⊥ = univ.pi fun i => Ioc (l i) (u i)

Tactic:
rw [coe_bot, univ_pi_eq_empty]

Result:
case neg.intro
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
⊢ Ioc (l ?m.45828) (u ?m.45828) = ∅

ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
⊢ ι

Proof state:
case pos
ι : Type u_1
l u : ι → ℝ
h : ∀ (i : ι), l i < u i
⊢ ↑↑{ lower := l, upper := u, lower_lt_upper := h } = univ.pi fun i => Ioc (l i) (u i)

Tactic:
exact coe_eq_pi _

Result:
no goals

Proof state:
case neg
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
⊢ ↑⊥ = univ.pi fun i => Ioc (l i) (u i)

Tactic:
rcases not_forall.mp h with ⟨i, hi⟩

Result:
case neg.intro
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
⊢ ↑⊥ = univ.pi fun i => Ioc (l i) (u i)

Proof state:
ι : Type u_1
l u : ι → ℝ
⊢ ↑(if h : ∀ (i : ι), l i < u i then ↑{ lower := l, upper := u, lower_lt_upper := h } else ⊥) =
    univ.pi fun i => Ioc (l i) (u i)

Tactic:
split_ifs with h

Result:
case pos
ι : Type u_1
l u : ι → ℝ
h : ∀ (i : ι), l i < u i
⊢ ↑↑{ lower := l, upper := u, lower_lt_upper := h } = univ.pi fun i => Ioc (l i) (u i)

case neg
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
⊢ ↑⊥ = univ.pi fun i => Ioc (l i) (u i)

Proof state:
ι : Type u_1
l u : ι → ℝ
⊢ ↑(mk' l u) = univ.pi fun i => Ioc (l i) (u i)

Tactic:
rw [mk']

Result:
ι : Type u_1
l u : ι → ℝ
⊢ ↑(if h : ∀ (i : ι), l i < u i then ↑{ lower := l, upper := u, lower_lt_upper := h } else ⊥) =
    univ.pi fun i => Ioc (l i) (u i)

Proof state:
case neg.intro
ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
⊢ Ioc (l ?m.45828) (u ?m.45828) = ∅

ι : Type u_1
l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
⊢ ι

Tactic:
exact Ioc_eq_empty hi

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem eqToHom_whiskerRight {X Y : C} (f : X = Y) (Z : C) :
    eqToHom f ▷ Z = eqToHom (congr_arg₂ tensorObj f rfl)

Proof state:
case refl
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Z : C
⊢ eqToHom ⋯ ▷ Z = eqToHom ⋯

Tactic:
simp only [id_whiskerRight, eqToHom_refl]

Result:
no goals

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X = Y
Z : C
⊢ eqToHom f ▷ Z = eqToHom ⋯

Tactic:
cases f

Result:
case refl
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Z : C
⊢ eqToHom ⋯ ▷ Z = eqToHom ⋯
-- Mathlib/Order/Filter/Map.lean
theorem disjoint_comap_iff (h : Surjective m) :
    Disjoint (comap m g₁) (comap m g₂) ↔ Disjoint g₁ g₂

Proof state:
α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
h : Surjective m
⊢ Disjoint (comap m g₁) (comap m g₂) ↔ Disjoint g₁ g₂

Tactic:
rw [disjoint_iff, disjoint_iff, ← comap_inf, comap_surjective_eq_bot h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List ((a : α) × β a)}
    {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Sigma.fst) :
    (m.insertMany l).getKey? k' = some k

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Sigma.fst l
⊢ (m.insertMany l).getKey? k' = some k

Tactic:
simp_to_raw using Raw₀.getKey?_insertMany_list_of_mem

Result:
no goals