harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/RCLike/Basic.lean
lemma instPosMulReflectLE : PosMulReflectLE K where
  elim a b c h

Proof state:
case intro.intro
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
h : ↑a * b ≤ ↑a * c
a' : ℝ
ha1 : a' > 0
ha2 : ↑a' = ↑a
⊢ b ≤ c

Tactic:
rw [← sub_nonneg]

Result:
case intro.intro
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
h : ↑a * b ≤ ↑a * c
a' : ℝ
ha1 : a' > 0
ha2 : ↑a' = ↑a
⊢ 0 ≤ c - b

Proof state:
case intro.intro
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
a' : ℝ
h : 0 < ↑a' * (c - b) ∨ 0 = ↑a' * (c - b)
ha1 : a' > 0
ha2 : ↑a' = ↑a
⊢ 0 ≤ c - b

Tactic:
rcases h with h | h

Result:
case intro.intro.inl
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
a' : ℝ
ha1 : a' > 0
ha2 : ↑a' = ↑a
h : 0 < ↑a' * (c - b)
⊢ 0 ≤ c - b

case intro.intro.inr
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
a' : ℝ
ha1 : a' > 0
ha2 : ↑a' = ↑a
h : 0 = ↑a' * (c - b)
⊢ 0 ≤ c - b

Proof state:
case intro.intro.inl
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
a' : ℝ
ha1 : a' > 0
ha2 : ↑a' = ↑a
h : 0 < ↑a' * (c - b)
⊢ 0 ≤ c - b

Tactic:
rw [ofReal_mul_pos_iff] at h

Result:
case intro.intro.inl
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
a' : ℝ
ha1 : a' > 0
ha2 : ↑a' = ↑a
h : a' < 0 ∧ c - b < 0 ∨ 0 < a' ∧ 0 < c - b
⊢ 0 ≤ c - b

Proof state:
case intro.intro
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
h : ↑a * b ≤ ↑a * c
a' : ℝ
ha1 : a' > 0
ha2 : ↑a' = ↑a
⊢ 0 ≤ c - b

Tactic:
rw [← ha2, ← sub_nonneg, ← mul_sub, le_iff_lt_or_eq] at h

Result:
case intro.intro
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
a' : ℝ
h : 0 < ↑a' * (c - b) ∨ 0 = ↑a' * (c - b)
ha1 : a' > 0
ha2 : ↑a' = ↑a
⊢ 0 ≤ c - b

Proof state:
case intro.intro.inr
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
a' : ℝ
ha1 : a' > 0
ha2 : ↑a' = ↑a
h : 0 = ↑a' * (c - b)
⊢ 0 ≤ c - b

Tactic:
exact ((mul_eq_zero_iff_left <| ofReal_ne_zero.mpr ha1.ne').mp h.symm).ge

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
h : ↑a * b ≤ ↑a * c
⊢ b ≤ c

Tactic:
obtain ⟨a', ha1, ha2⟩ := pos_iff_exists_ofReal.mp a.2

Result:
case intro.intro
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
h : ↑a * b ≤ ↑a * c
a' : ℝ
ha1 : a' > 0
ha2 : ↑a' = ↑a
⊢ b ≤ c
-- Mathlib/Data/Rat/Defs.lean
@[simp] lemma divInt_self' {n : ℤ} (hn : n ≠ 0) : n /. n = 1

Proof state:
n : ℤ
hn : n ≠ 0
⊢ n /. n = 1

Tactic:
simpa using divInt_mul_right (n := 1) (d := 1) hn

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/QuasiIso.lean
lemma quasiIso_of_comp_left (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃)
    [hφ : QuasiIso φ] [hφφ' : QuasiIso (φ ≫ φ')] :
    QuasiIso φ'

Proof state:
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : IsIso (homologyMap φ)
hφφ' : IsIso (homologyMap φ ≫ homologyMap φ')
⊢ IsIso (homologyMap φ')

Tactic:
exact IsIso.of_isIso_comp_left (homologyMap φ) (homologyMap φ')

Result:
no goals

Proof state:
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : IsIso (homologyMap φ)
hφφ' : IsIso (homologyMap (φ ≫ φ'))
⊢ IsIso (homologyMap φ')

Tactic:
rw [homologyMap_comp] at hφφ'

Result:
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : IsIso (homologyMap φ)
hφφ' : IsIso (homologyMap φ ≫ homologyMap φ')
⊢ IsIso (homologyMap φ')

Proof state:
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : QuasiIso φ
hφφ' : QuasiIso (φ ≫ φ')
⊢ QuasiIso φ'

Tactic:
rw [quasiIso_iff] at hφ hφφ' ⊢

Result:
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : IsIso (homologyMap φ)
hφφ' : IsIso (homologyMap (φ ≫ φ'))
⊢ IsIso (homologyMap φ')
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
/-- If `M` is a commutative group that contains a primitive `n`th root of unity
and `a : ZMod n` is nonzero, then there exists a group homomorphism `φ` from the
additive group `ZMod n` to the multiplicative group `Mˣ` such that `φ a ≠ 1`. -/
lemma ZMod.exists_monoidHom_apply_ne_one {M : Type*} [CommMonoid M] {n : ℕ} [NeZero n]
    (hG : ∃ ζ : M, IsPrimitiveRoot ζ n) {a : ZMod n} (ha : a ≠ 0) :
    ∃ φ : Multiplicative (ZMod n) →* Mˣ, φ (Multiplicative.ofAdd a) ≠ 1

Proof state:
M : Type u_7
inst✝¹ : CommMonoid M
n : ℕ
inst✝ : NeZero n
a : ZMod n
ha : a ≠ 0
ζ : M
hζ : IsPrimitiveRoot ζ n
⊢ n = Nat.card (Multiplicative (ZMod n))

Tactic:
simp only [Nat.card_eq_fintype_card, Fintype.card_multiplicative, card]

Result:
no goals

Proof state:
M : Type u_7
inst✝¹ : CommMonoid M
n : ℕ
inst✝ : NeZero n
a : ZMod n
ha : a ≠ 0
ζ : M
hζ : IsPrimitiveRoot ζ n
hc : n = Nat.card (Multiplicative (ZMod n))
⊢ Multiplicative.ofAdd a ≠ 1

Tactic:
simp only [ne_eq, ofAdd_eq_one, ha, not_false_eq_true]

Result:
no goals

Proof state:
M : Type u_7
inst✝¹ : CommMonoid M
n : ℕ
inst✝ : NeZero n
hG : ∃ ζ, IsPrimitiveRoot ζ n
a : ZMod n
ha : a ≠ 0
⊢ ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1

Tactic:
obtain ⟨ζ, hζ⟩ := hG

Result:
case intro
M : Type u_7
inst✝¹ : CommMonoid M
n : ℕ
inst✝ : NeZero n
a : ZMod n
ha : a ≠ 0
ζ : M
hζ : IsPrimitiveRoot ζ n
⊢ ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1

Proof state:
case intro
M : Type u_7
inst✝¹ : CommMonoid M
n : ℕ
inst✝ : NeZero n
a : ZMod n
ha : a ≠ 0
ζ : M
hζ : IsPrimitiveRoot ζ n
⊢ ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1

Tactic:
have hc : n = Nat.card (Multiplicative (ZMod n)) := by
  simp only [Nat.card_eq_fintype_card, Fintype.card_multiplicative, card]

Result:
case intro
M : Type u_7
inst✝¹ : CommMonoid M
n : ℕ
inst✝ : NeZero n
a : ZMod n
ha : a ≠ 0
ζ : M
hζ : IsPrimitiveRoot ζ n
hc : n = Nat.card (Multiplicative (ZMod n))
⊢ ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1

Proof state:
case intro
M : Type u_7
inst✝¹ : CommMonoid M
n : ℕ
inst✝ : NeZero n
a : ZMod n
ha : a ≠ 0
ζ : M
hζ : IsPrimitiveRoot ζ n
hc : n = Nat.card (Multiplicative (ZMod n))
⊢ ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1

Tactic:
exact IsCyclic.exists_apply_ne_one
  (hc ▸ ⟨hζ.toRootsOfUnity.val, IsPrimitiveRoot.coe_units_iff.mp hζ⟩) <|
  by simp only [ne_eq, ofAdd_eq_one, ha, not_false_eq_true]

Result:
no goals
-- Mathlib/Data/Rat/Lemmas.lean
theorem exists_eq_mul_div_num_and_eq_mul_div_den (n : ℤ) {d : ℤ} (d_ne_zero : d ≠ 0) :
    ∃ c : ℤ, n = c * ((n : ℚ) / d).num ∧ (d : ℤ) = c * ((n : ℚ) / d).den :=
  haveI : (n : ℚ) / d = Rat.divInt n d

Proof state:
n d : ℤ
d_ne_zero : d ≠ 0
⊢ ↑n / ↑d = n /. d

Tactic:
rw [← Rat.divInt_eq_div]

Result:
no goals
-- Mathlib/Tactic/Positivity/Core.lean
lemma nonneg_of_isNat {n : ℕ} [OrderedSemiring A]
    (h : NormNum.IsNat e n) : 0 ≤ (e : A)

Proof state:
A : Type u_1
e : A
n : ℕ
inst✝ : OrderedSemiring A
h : NormNum.IsNat e n
⊢ 0 ≤ ↑n

Tactic:
exact Nat.cast_nonneg n

Result:
no goals

Proof state:
A : Type u_1
e : A
n : ℕ
inst✝ : OrderedSemiring A
h : NormNum.IsNat e n
⊢ 0 ≤ e

Tactic:
rw [NormNum.IsNat.to_eq h rfl]

Result:
A : Type u_1
e : A
n : ℕ
inst✝ : OrderedSemiring A
h : NormNum.IsNat e n
⊢ 0 ≤ ↑n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem cond_false_not_same : ∀ (c b : Bool), cond c b (!c) = (!c || b)

Proof state:
⊢ ∀ (c b : Bool), (bif c then b else !c) = (!c || b)

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem coe_neg_one : ↑(-1 : Fin (n + 1)) = n

Proof state:
case succ
n✝ : ℕ
⊢ ↑(-1) = n✝ + 1

Tactic:
rw [Fin.coe_neg, Fin.val_one, Nat.add_one_sub_one, Nat.mod_eq_of_lt]

Result:
case succ
n✝ : ℕ
⊢ n✝ + 1 < n✝ + 1 + 1

Proof state:
case succ
n✝ : ℕ
⊢ n✝ + 1 < n✝ + 1 + 1

Tactic:
constructor

Result:
no goals

Proof state:
case zero

⊢ ↑(-1) = 0

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ ↑(-1) = n

Tactic:
cases n

Result:
case zero

⊢ ↑(-1) = 0

case succ
n✝ : ℕ
⊢ ↑(-1) = n✝ + 1
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem dist_mul_self_right (a b : E) : dist b (a * b) = ‖a‖

Proof state:
E : Type u_2
inst✝ : SeminormedGroup E
a b : E
⊢ dist b (a * b) = ‖a‖

Tactic:
rw [← dist_one_left, ← dist_mul_right 1 a b, one_mul]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean
theorem exists_int_eq_of_partDen {b : K}
    (nth_partDen_eq : (of v).partDens.get? n = some b) : ∃ z : ℤ, b = (z : K)

Proof state:
case intro.intro
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
gp_b_eq_b_n : gp.b = b
this : ∃ z, gp.b = ↑z
⊢ ∃ z, b = ↑z

Tactic:
rwa [gp_b_eq_b_n] at this

Result:
no goals

Proof state:
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
⊢ ∃ z, b = ↑z

Tactic:
obtain ⟨gp, nth_s_eq, gp_b_eq_b_n⟩ : ∃ gp, (of v).s.get? n = some gp ∧ gp.b = b :=
  exists_s_b_of_partDen nth_partDen_eq

Result:
case intro.intro
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
gp_b_eq_b_n : gp.b = b
⊢ ∃ z, b = ↑z

Proof state:
case intro.intro
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
gp_b_eq_b_n : gp.b = b
⊢ ∃ z, b = ↑z

Tactic:
have : ∃ z : ℤ, gp.b = (z : K) := (of_partNum_eq_one_and_exists_int_partDen_eq nth_s_eq).right

Result:
case intro.intro
K : Type u_1
v : K
n : ℕ
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
gp_b_eq_b_n : gp.b = b
this : ∃ z, gp.b = ↑z
⊢ ∃ z, b = ↑z
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem neg_mul_emod_left (a b : Int) : -(a * b) % b = 0

Proof state:
a b : Int
⊢ b ∣ a * b

Tactic:
exact Int.dvd_mul_left a b

Result:
no goals

Proof state:
a b : Int
⊢ -(a * b) % b = 0

Tactic:
rw [← dvd_iff_emod_eq_zero, Int.dvd_neg]

Result:
a b : Int
⊢ b ∣ a * b
-- Mathlib/Data/Fin/Basic.lean
lemma natCast_lt_natCast (han : a ≤ n) (hbn : b ≤ n) : (a : Fin (n + 1)) < b ↔ a < b

Proof state:
n a b : ℕ
han : a ≤ n
hbn : b ≤ n
⊢ ↑a < ↑b ↔ a < b

Tactic:
rw [← Nat.lt_succ_iff] at han hbn

Result:
n a b : ℕ
han : a < n.succ
hbn : b < n.succ
⊢ ↑a < ↑b ↔ a < b

Proof state:
n a b : ℕ
han : a < n.succ
hbn : b < n.succ
⊢ ↑a < ↑b ↔ a < b

Tactic:
simp [lt_iff_val_lt_val, Nat.mod_eq_of_lt, han, hbn]

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem Products.span_nil_eq_top {I} [LinearOrder I] :
    Submodule.span ℤ (eval ({fun _ ↦ false} : Set (I → Bool)) '' {nil}) = ⊤

Proof state:
I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x => false} ℤ
a✝ : f ∈ ⊤
x : ↑{fun x => false}
⊢ x = default

Tactic:
simp only [Set.default_coe_singleton, eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x => false} ℤ
a✝ : f ∈ ⊤
⊢ ∃ a, a • eval {fun x => false} nil = f

Tactic:
refine ⟨f default, ?_⟩

Result:
I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x => false} ℤ
a✝ : f ∈ ⊤
⊢ f default • eval {fun x => false} nil = f

Proof state:
I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x => false} ℤ
a✝ : f ∈ ⊤
⊢ ↑(f default) = f

Tactic:
ext x

Result:
case h
I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x => false} ℤ
a✝ : f ∈ ⊤
x : ↑{fun x => false}
⊢ ↑(f default) x = f x

Proof state:
I : Type u_1
inst✝ : LinearOrder I
⊢ Submodule.span ℤ (eval {fun x => false} '' {nil}) = ⊤

Tactic:
rw [Set.image_singleton, eq_top_iff]

Result:
I : Type u_1
inst✝ : LinearOrder I
⊢ ⊤ ≤ Submodule.span ℤ {eval {fun x => false} nil}

Proof state:
case h
I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x => false} ℤ
a✝ : f ∈ ⊤
⊢ ↑(f default) default = f default

Tactic:
rfl

Result:
no goals

Proof state:
I : Type u_1
inst✝ : LinearOrder I
⊢ ⊤ ≤ Submodule.span ℤ {eval {fun x => false} nil}

Tactic:
intro f _

Result:
I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x => false} ℤ
a✝ : f ∈ ⊤
⊢ f ∈ Submodule.span ℤ {eval {fun x => false} nil}

Proof state:
case h
I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x => false} ℤ
a✝ : f ∈ ⊤
x : ↑{fun x => false}
⊢ ↑(f default) x = f x

Tactic:
obtain rfl : x = default := by simp only [Set.default_coe_singleton, eq_iff_true_of_subsingleton]

Result:
case h
I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x => false} ℤ
a✝ : f ∈ ⊤
⊢ ↑(f default) default = f default

Proof state:
I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x => false} ℤ
a✝ : f ∈ ⊤
⊢ f default • eval {fun x => false} nil = f

Tactic:
simp only [eval, List.map, List.prod_nil, zsmul_eq_mul, mul_one, Products.nil]

Result:
I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x => false} ℤ
a✝ : f ∈ ⊤
⊢ ↑(f default) = f

Proof state:
I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x => false} ℤ
a✝ : f ∈ ⊤
⊢ f ∈ Submodule.span ℤ {eval {fun x => false} nil}

Tactic:
rw [Submodule.mem_span_singleton]

Result:
I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x => false} ℤ
a✝ : f ∈ ⊤
⊢ ∃ a, a • eval {fun x => false} nil = f
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive (attr := simp)]
lemma stabilizer_mul_self (s : Set G) : (stabilizer G s : Set G) * s = s

Proof state:
case h.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
s : Set G
a : G
ha : a ∈ ↑(stabilizer G s)
b : G
hb : b ∈ s
⊢ (fun x1 x2 => x1 * x2) a b ∈ a • s

Tactic:
exact smul_mem_smul_set hb

Result:
no goals

Proof state:
case h
G : Type u_1
inst✝ : Group G
s : Set G
x✝ : G
⊢ x✝ ∈ ↑(stabilizer G s) * s → x✝ ∈ s

Tactic:
rintro ⟨a, ha, b, hb, rfl⟩

Result:
case h.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
s : Set G
a : G
ha : a ∈ ↑(stabilizer G s)
b : G
hb : b ∈ s
⊢ (fun x1 x2 => x1 * x2) a b ∈ s

Proof state:
case h
G : Type u_1
inst✝ : Group G
s : Set G
x✝ : G
⊢ x✝ ∈ ↑(stabilizer G s) * s ↔ x✝ ∈ s

Tactic:
refine ⟨?_, fun h ↦ ⟨_, (stabilizer G s).one_mem, _, h, one_mul _⟩⟩

Result:
case h
G : Type u_1
inst✝ : Group G
s : Set G
x✝ : G
⊢ x✝ ∈ ↑(stabilizer G s) * s → x✝ ∈ s

Proof state:
case h.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
s : Set G
a : G
ha : a ∈ ↑(stabilizer G s)
b : G
hb : b ∈ s
⊢ (fun x1 x2 => x1 * x2) a b ∈ s

Tactic:
rw [← mem_stabilizer_iff.1 ha]

Result:
case h.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
s : Set G
a : G
ha : a ∈ ↑(stabilizer G s)
b : G
hb : b ∈ s
⊢ (fun x1 x2 => x1 * x2) a b ∈ a • s

Proof state:
G : Type u_1
inst✝ : Group G
s : Set G
⊢ ↑(stabilizer G s) * s = s

Tactic:
ext

Result:
case h
G : Type u_1
inst✝ : Group G
s : Set G
x✝ : G
⊢ x✝ ∈ ↑(stabilizer G s) * s ↔ x✝ ∈ s
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/GaussSum.lean
theorem quadraticChar_neg_two [DecidableEq F] (hF : ringChar F ≠ 2) :
    quadraticChar F (-2) = χ₈' (Fintype.card F)

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ (quadraticChar F) (-2) = χ₈' ↑(Fintype.card F)

Tactic:
rw [(by norm_num : (-2 : F) = -1 * 2), map_mul, χ₈'_eq_χ₄_mul_χ₈, quadraticChar_neg_one hF,
  quadraticChar_two hF, @cast_natCast _ (ZMod 4) _ _ _ (by decide : 4 ∣ 8)]

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ -2 = -1 * 2

Tactic:
norm_num

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ 4 ∣ 8

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Order/Group/Multiset.lean
lemma mem_nsmul_of_ne_zero {a : α} {s : Multiset α} {n : ℕ} (h0 : n ≠ 0) : a ∈ n • s ↔ a ∈ s

Proof state:
α : Type u_1
a : α
s : Multiset α
n : ℕ
h0 : n ≠ 0
⊢ a ∈ n • s ↔ a ∈ s

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Order/OmegaCompletePartialOrder.lean
theorem ωSup_le_iff {c : Chain α} {x : α} : ωSup c ≤ x ↔ ∀ i, c i ≤ x

Proof state:
case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ∀ (i : ℕ), c i ≤ x
⊢ ωSup c ≤ x

Tactic:
exact ωSup_le _ _ ‹_›

Result:
no goals

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ ωSup c ≤ x

Tactic:
assumption

Result:
no goals

Proof state:
case mp
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ c i✝ ≤ x

Tactic:
trans ωSup c

Result:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ c i✝ ≤ ωSup c

α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ ωSup c ≤ x

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ c i✝ ≤ ωSup c

Tactic:
exact le_ωSup _ _

Result:
no goals

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
⊢ ωSup c ≤ x ↔ ∀ (i : ℕ), c i ≤ x

Tactic:
constructor <;> intros

Result:
case mp
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ c i✝ ≤ x

case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ∀ (i : ℕ), c i ≤ x
⊢ ωSup c ≤ x
-- Mathlib/FieldTheory/Relrank.lean
theorem lift_relrank_map_map (f : E →+* L) :
    lift.{v} (relrank (A.map f) (B.map f)) = lift.{w} (relrank A B) :=
  -- typeclass inference is slow
  .symm <| Algebra.lift_rank_eq_of_equiv_equiv (((A ⊓ B).equivMapOfInjective f f.injective).trans
    <| .subringCongr <| by rw [← map_inf]; rfl) (B.equivMapOfInjective f f.injective) rfl

Proof state:
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : E →+* L
⊢ Subring.map f (A ⊓ B).toSubring = (map f A ⊓ map f B).toSubring

Tactic:
rw [← map_inf]

Result:
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : E →+* L
⊢ Subring.map f (A ⊓ B).toSubring = (map f (A ⊓ B)).toSubring

Proof state:
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : E →+* L
⊢ Subring.map f (A ⊓ B).toSubring = (map f (A ⊓ B)).toSubring

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem integralPowerBasis_gen [hcycl : IsCyclotomicExtension {p ^ k} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) :
    hζ.integralPowerBasis.gen = hζ.toInteger :=
  Subtype.ext <| show algebraMap _ K hζ.integralPowerBasis.gen = _ by
    rw [integralPowerBasis, PowerBasis.map_gen, adjoin.powerBasis'_gen]
    simp only [adjoinEquivRingOfIntegers_apply, IsIntegralClosure.algebraMap_lift]
    rfl

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ (algebraMap (𝓞 K) K) hζ.integralPowerBasis.gen = ↑hζ.toInteger

Tactic:
rw [integralPowerBasis, PowerBasis.map_gen, adjoin.powerBasis'_gen]

Result:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ (algebraMap (𝓞 K) K) (hζ.adjoinEquivRingOfIntegers ⟨ζ, ⋯⟩) = ↑hζ.toInteger

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ (algebraMap (𝓞 K) K) (hζ.adjoinEquivRingOfIntegers ⟨ζ, ⋯⟩) = ↑hζ.toInteger

Tactic:
simp only [adjoinEquivRingOfIntegers_apply, IsIntegralClosure.algebraMap_lift]

Result:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ (algebraMap (↥(adjoin ℤ {ζ})) K) ⟨ζ, ⋯⟩ = ζ

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ (algebraMap (↥(adjoin ℤ {ζ})) K) ⟨ζ, ⋯⟩ = ζ

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/FreeCommRing.lean
theorem coe_surjective : Surjective ((↑) : FreeRing α → FreeCommRing α) := fun x => by
  induction x with
  | hn1 =>
    use -1
    rfl
  | hb b =>
    exact ⟨FreeRing.of b, rfl⟩
  | ha _ _ hx hy =>
    rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
    exact ⟨x + y, (FreeRing.lift _).map_add _ _⟩
  | hm _ _ hx hy =>
    rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
    exact ⟨x * y, (FreeRing.lift _).map_mul _ _⟩

Proof state:
case ha
α : Type u
x✝ y✝ : FreeCommRing α
hx : ∃ a, ↑a = x✝
hy : ∃ a, ↑a = y✝
⊢ ∃ a, ↑a = x✝ + y✝

Tactic:
rcases hx with ⟨x, rfl⟩

Result:
case ha.intro
α : Type u
y✝ : FreeCommRing α
hy : ∃ a, ↑a = y✝
x : FreeRing α
⊢ ∃ a, ↑a = ↑x + y✝

Proof state:
case ha.intro
α : Type u
y✝ : FreeCommRing α
hy : ∃ a, ↑a = y✝
x : FreeRing α
⊢ ∃ a, ↑a = ↑x + y✝

Tactic:
rcases hy with ⟨y, rfl⟩

Result:
case ha.intro.intro
α : Type u
x y : FreeRing α
⊢ ∃ a, ↑a = ↑x + ↑y

Proof state:
case hm.intro
α : Type u
y✝ : FreeCommRing α
hy : ∃ a, ↑a = y✝
x : FreeRing α
⊢ ∃ a, ↑a = ↑x * y✝

Tactic:
rcases hy with ⟨y, rfl⟩

Result:
case hm.intro.intro
α : Type u
x y : FreeRing α
⊢ ∃ a, ↑a = ↑x * ↑y

Proof state:
case hm
α : Type u
x✝ y✝ : FreeCommRing α
hx : ∃ a, ↑a = x✝
hy : ∃ a, ↑a = y✝
⊢ ∃ a, ↑a = x✝ * y✝

Tactic:
rcases hx with ⟨x, rfl⟩

Result:
case hm.intro
α : Type u
y✝ : FreeCommRing α
hy : ∃ a, ↑a = y✝
x : FreeRing α
⊢ ∃ a, ↑a = ↑x * y✝

Proof state:
case hb
α : Type u
b : α
⊢ ∃ a, ↑a = FreeCommRing.of b

Tactic:
exact ⟨FreeRing.of b, rfl⟩

Result:
no goals

Proof state:
case ha.intro.intro
α : Type u
x y : FreeRing α
⊢ ∃ a, ↑a = ↑x + ↑y

Tactic:
exact ⟨x + y, (FreeRing.lift _).map_add _ _⟩

Result:
no goals

Proof state:
case h
α : Type u
⊢ ↑(-1) = -1

Tactic:
rfl

Result:
no goals

Proof state:
case hm.intro.intro
α : Type u
x y : FreeRing α
⊢ ∃ a, ↑a = ↑x * ↑y

Tactic:
exact ⟨x * y, (FreeRing.lift _).map_mul _ _⟩

Result:
no goals

Proof state:
α : Type u
x : FreeCommRing α
⊢ ∃ a, ↑a = x

Tactic:
induction x with
| hn1 =>
  use -1
  rfl
| hb b =>
  exact ⟨FreeRing.of b, rfl⟩
| ha _ _ hx hy =>
  rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
  exact ⟨x + y, (FreeRing.lift _).map_add _ _⟩
| hm _ _ hx hy =>
  rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
  exact ⟨x * y, (FreeRing.lift _).map_mul _ _⟩

Result:
no goals

Proof state:
case hn1
α : Type u
⊢ ∃ a, ↑a = -1

Tactic:
use -1

Result:
case h
α : Type u
⊢ ↑(-1) = -1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_reverse (a : Vector α n) (i : Nat) (hi : i < n) :
    (a.reverse)[i] = a[n - 1 - i]

Proof state:
case mk
α : Type u_1
i : Nat
a : Array α
hi : i < a.size
⊢ { toArray := a, size_toArray := ⋯ }.reverse[i] = { toArray := a, size_toArray := ⋯ }[a.size - 1 - i]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : Vector α n
i : Nat
hi : i < n
⊢ a.reverse[i] = a[n - 1 - i]

Tactic:
rcases a with ⟨a, rfl⟩

Result:
case mk
α : Type u_1
i : Nat
a : Array α
hi : i < a.size
⊢ { toArray := a, size_toArray := ⋯ }.reverse[i] = { toArray := a, size_toArray := ⋯ }[a.size - 1 - i]