harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem _root_.Complex.rotation (θ : Real.Angle) (z : ℂ) :
    Complex.orientation.rotation θ z = θ.toCircle * z

Proof state:
θ : Real.Angle
z : ℂ
⊢ (Complex.orientation.rotation θ) z = ↑θ.toCircle * z

Tactic:
simp only [rotation_apply, Complex.rightAngleRotation, Real.Angle.coe_toCircle, real_smul]

Result:
θ : Real.Angle
z : ℂ
⊢ ↑θ.cos * z + ↑θ.sin * (I * z) = (↑θ.cos + ↑θ.sin * I) * z

Proof state:
θ : Real.Angle
z : ℂ
⊢ ↑θ.cos * z + ↑θ.sin * (I * z) = (↑θ.cos + ↑θ.sin * I) * z

Tactic:
ring

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem cos_oangle_right_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) :
    Real.Angle.cos (∡ p₂ p₃ p₁) = dist p₃ p₂ / dist p₁ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ (∡ p₂ p₃ p₁).cos = dist p₃ p₂ / dist p₁ p₃

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
  cos_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₂ p₃ p₁).cos = dist p₃ p₂ / dist p₁ p₃

Tactic:
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₂ p₃ p₁).sign = 1
⊢ (∡ p₂ p₃ p₁).cos = dist p₃ p₂ / dist p₁ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₂ p₃ p₁).sign = 1

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

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem dimH_bUnion {s : Set ι} (hs : s.Countable) (t : ι → Set X) :
    dimH (⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH (t i)

Proof state:
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
s : Set ι
hs : s.Countable
t : ι → Set X
⊢ dimH (⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH (t i)

Tactic:
haveI := hs.toEncodable

Result:
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
s : Set ι
hs : s.Countable
t : ι → Set X
this : Encodable ↑s
⊢ dimH (⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH (t i)

Proof state:
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
s : Set ι
hs : s.Countable
t : ι → Set X
this : Encodable ↑s
⊢ dimH (⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH (t i)

Tactic:
rw [biUnion_eq_iUnion, dimH_iUnion, ← iSup_subtype'']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.or_true (b : Bool) : (b || true) = true

Proof state:
b : Bool
⊢ (b || true) = true

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/Data/ZMod/ValMinAbs.lean
lemma valMinAbs_nonneg_iff [NeZero n] (x : ZMod n) : 0 ≤ x.valMinAbs ↔ x.val ≤ n / 2

Proof state:
case neg
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬x.val ≤ n / 2
⊢ 0 ≤ ↑x.val - ↑n ↔ x.val ≤ n / 2

Tactic:
exact iff_of_false (sub_lt_zero.2 <| Int.ofNat_lt.2 x.val_lt).not_le h

Result:
no goals

Proof state:
case pos
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.val ≤ n / 2
⊢ 0 ≤ ↑x.val ↔ x.val ≤ n / 2

Tactic:
exact iff_of_true (Nat.cast_nonneg _) h

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ (0 ≤ if x.val ≤ n / 2 then ↑x.val else ↑x.val - ↑n) ↔ x.val ≤ n / 2

Tactic:
split_ifs with h

Result:
case pos
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : x.val ≤ n / 2
⊢ 0 ≤ ↑x.val ↔ x.val ≤ n / 2

case neg
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬x.val ≤ n / 2
⊢ 0 ≤ ↑x.val - ↑n ↔ x.val ≤ n / 2

Proof state:
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ 0 ≤ x.valMinAbs ↔ x.val ≤ n / 2

Tactic:
rw [valMinAbs_def_pos]

Result:
n : ℕ
inst✝ : NeZero n
x : ZMod n
⊢ (0 ≤ if x.val ≤ n / 2 then ↑x.val else ↑x.val - ↑n) ↔ x.val ≤ n / 2
-- Mathlib/Analysis/Asymptotics/Theta.lean
theorem isTheta_inv {f : α → 𝕜} {g : α → 𝕜'} :
    ((fun x ↦ (f x)⁻¹) =Θ[l] fun x ↦ (g x)⁻¹) ↔ f =Θ[l] g :=
  ⟨fun h ↦ by simpa only [inv_inv] using h.inv, IsTheta.inv⟩

Proof state:
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : (fun x => (f x)⁻¹) =Θ[l] fun x => (g x)⁻¹
⊢ f =Θ[l] g

Tactic:
simpa only [inv_inv] using h.inv

Result:
no goals
-- Mathlib/Data/W/Constructions.lean
theorem rightInverse_list : Function.RightInverse (ofList γ) (toList _)
  | List.nil => rfl
  | List.cons hd tl => by simp [rightInverse_list tl]

Proof state:
γ : Type u
hd : γ
tl : List γ
⊢ toList γ (ofList γ (hd :: tl)) = hd :: tl

Tactic:
simp [rightInverse_list tl]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean
theorem inl_comp_pushoutSymmetry_inv [HasPushout f g] :
    pushout.inl _ _ ≫ (pushoutSymmetry f g).inv = pushout.inr _ _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ pushout.inl g f ≫ (pushoutSymmetry f g).inv = pushout.inr f g

Tactic:
simp [Iso.comp_inv_eq]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
@[norm_cast, to_additive]
lemma coe_set_eq_one [Group G] {s : Subgroup G} : (s : Set G) = 1 ↔ s = ⊥ :=
  (SetLike.ext'_iff.trans (by rfl)).symm

Proof state:
G : Type u_2
inst✝ : Group G
s : Subgroup G
⊢ ↑s = ↑⊥ ↔ ↑s = 1

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finset/Sym.lean
theorem image_diag_union_image_offDiag [DecidableEq α] :
    s.diag.image Sym2.mk ∪ s.offDiag.image Sym2.mk = s.sym2

Proof state:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ image Sym2.mk s.diag ∪ image Sym2.mk s.offDiag = s.sym2

Tactic:
rw [← image_union, diag_union_offDiag, sym2_eq_image]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MinMax.lean
theorem isSome_max?_of_mem {l : List α} [Max α] {a : α} (h : a ∈ l) :
    l.max?.isSome

Proof state:
α : Type u_1
l : List α
inst✝ : Max α
a : α
h : a ∈ l
⊢ l.max?.isSome = true

Tactic:
cases l <;> simp_all [List.max?_cons']

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem log_b_ne_zero : log b ≠ 0

Proof state:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
b_ne_zero : b ≠ 0
⊢ log b ≠ 0

Tactic:
have b_ne_minus_one : b ≠ -1 := by linarith

Result:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
b_ne_zero : b ≠ 0
b_ne_minus_one : b ≠ -1
⊢ log b ≠ 0

Proof state:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ b ≠ 0

Tactic:
linarith

Result:
no goals

Proof state:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
b_ne_zero : b ≠ 0
b_ne_minus_one : b ≠ -1
⊢ log b ≠ 0

Tactic:
simp [b_ne_one, b_ne_zero, b_ne_minus_one]

Result:
no goals

Proof state:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ log b ≠ 0

Tactic:
have b_ne_zero : b ≠ 0 := by linarith

Result:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
b_ne_zero : b ≠ 0
⊢ log b ≠ 0

Proof state:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
b_ne_zero : b ≠ 0
⊢ b ≠ -1

Tactic:
linarith

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
/-- We can shrink a set to any smaller size. -/
lemma exists_subset_card_eq (hns : n ≤ #s) : ∃ t ⊆ s, #t = n

Proof state:
α : Type u_1
s : Finset α
n : ℕ
hns : n ≤ #s
⊢ ∃ t ⊆ s, #t = n

Tactic:
simpa using exists_subsuperset_card_eq s.empty_subset (by simp) hns

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
n : ℕ
hns : n ≤ #s
⊢ #∅ ≤ n

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
theorem spanNorm_eq_bot_iff {I : Ideal S} : spanNorm R I = ⊥ ↔ I = ⊥

Proof state:
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
I : Ideal S
⊢ spanNorm R I = ⊥ ↔ I = ⊥

Tactic:
simp only [spanNorm, span_eq_bot, Set.mem_image, SetLike.mem_coe, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂, Algebra.intNorm_eq_zero, @eq_bot_iff _ _ _ I, SetLike.le_def, map,
  mem_bot]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Impl.lean
theorem flatten_eq_flattenTR : @flatten = @flattenTR

Proof state:
case h.h
α : Type u_1
l : List (List α)
⊢ l.flatten = l.flattenTR

Tactic:
rw [← List.flatMap_id, List.flatMap_eq_flatMapTR]

Result:
case h.h
α : Type u_1
l : List (List α)
⊢ flatMapTR id l = l.flattenTR

Proof state:
⊢ @flatten = @flattenTR

Tactic:
funext α l

Result:
case h.h
α : Type u_1
l : List (List α)
⊢ l.flatten = l.flattenTR

Proof state:
case h.h
α : Type u_1
l : List (List α)
⊢ flatMapTR id l = l.flattenTR

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
@[to_additive (attr := simp)]
lemma smul_coe_set [Group G] [SetLike S G] [SubgroupClass S G] {s : S} {a : G} (ha : a ∈ s) :
    a • (s : Set G) = s

Proof state:
case h
G : Type u_2
S : Type u_4
inst✝² : Group G
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
s : S
a : G
ha : a ∈ s
x✝ : G
⊢ x✝ ∈ a • ↑s ↔ x✝ ∈ ↑s

Tactic:
simp [Set.mem_smul_set_iff_inv_smul_mem, mul_mem_cancel_left, ha]

Result:
no goals

Proof state:
G : Type u_2
S : Type u_4
inst✝² : Group G
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
s : S
a : G
ha : a ∈ s
⊢ a • ↑s = ↑s

Tactic:
ext

Result:
case h
G : Type u_2
S : Type u_4
inst✝² : Group G
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
s : S
a : G
ha : a ∈ s
x✝ : G
⊢ x✝ ∈ a • ↑s ↔ x✝ ∈ ↑s
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem natDegree_lt_natDegree_iff (hp : p ≠ 0) : natDegree p < natDegree q ↔ degree p < degree q :=
  ⟨degree_lt_degree, fun h ↦ by
    have hq : q ≠ 0 := ne_zero_of_degree_gt h
    rwa [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt] at h⟩

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p ≠ 0
h : p.degree < q.degree
⊢ p.natDegree < q.natDegree

Tactic:
have hq : q ≠ 0 := ne_zero_of_degree_gt h

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p ≠ 0
h : p.degree < q.degree
hq : q ≠ 0
⊢ p.natDegree < q.natDegree

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p ≠ 0
h : p.degree < q.degree
hq : q ≠ 0
⊢ p.natDegree < q.natDegree

Tactic:
rwa [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt] at h

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean
theorem ofBaseChange_comp_toBaseChange (Q : QuadraticForm R V) :
    (ofBaseChange A Q).comp (toBaseChange A Q) = AlgHom.id _ _

Proof state:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
⊢ (ofBaseChange A Q).comp (toBaseChange A Q) = AlgHom.id A (CliffordAlgebra (QuadraticForm.baseChange A Q))

Tactic:
ext x

Result:
case a.a.h.h
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
x : V
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (((ofBaseChange A Q).comp (toBaseChange A Q)).toLinearMap ∘ₗ ι (QuadraticForm.baseChange A Q)))
        1)
      x =
    ((TensorProduct.AlgebraTensorModule.curry
          ((AlgHom.id A (CliffordAlgebra (QuadraticForm.baseChange A Q))).toLinearMap ∘ₗ
            ι (QuadraticForm.baseChange A Q)))
        1)
      x

Proof state:
case a.a.h.h
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
x : V
⊢ (ofBaseChange A Q) ((toBaseChange A Q) ((ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] x))) =
    (ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] x)

Tactic:
rw [toBaseChange_ι, ofBaseChange_tmul_ι]

Result:
no goals

Proof state:
case a.a.h.h
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
x : V
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (((ofBaseChange A Q).comp (toBaseChange A Q)).toLinearMap ∘ₗ ι (QuadraticForm.baseChange A Q)))
        1)
      x =
    ((TensorProduct.AlgebraTensorModule.curry
          ((AlgHom.id A (CliffordAlgebra (QuadraticForm.baseChange A Q))).toLinearMap ∘ₗ
            ι (QuadraticForm.baseChange A Q)))
        1)
      x

Tactic:
show ofBaseChange A Q (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] x)))
  = ι (Q.baseChange A) (1 ⊗ₜ[R] x)

Result:
case a.a.h.h
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
x : V
⊢ (ofBaseChange A Q) ((toBaseChange A Q) ((ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] x))) =
    (ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] x)
-- Mathlib/Algebra/Order/Floor.lean
theorem fract_add_nat (a : α) (m : ℕ) : fract (a + m) = fract a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
m : ℕ
⊢ a + ↑m - ↑⌊a + ↑m⌋ = fract a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
m : ℕ
⊢ fract (a + ↑m) = fract a

Tactic:
rw [fract]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
m : ℕ
⊢ a + ↑m - ↑⌊a + ↑m⌋ = fract a
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem prod_set :
    ∀ (L : List M) (n : ℕ) (a : M),
      (L.set n a).prod =
        ((L.take n).prod * if n < L.length then a else 1) * (L.drop (n + 1)).prod
  | x :: xs, 0, a => by simp [set]
  | x :: xs, i + 1, a => by
    simp [set, prod_set xs i a, mul_assoc, Nat.add_lt_add_iff_right]
  | [], _, _ => by simp [set, (Nat.zero_le _).not_lt, Nat.zero_le]

Proof state:
M : Type u_4
inst✝ : Monoid M
x : M
xs : List M
a : M
⊢ ((x :: xs).set 0 a).prod =
    ((take 0 (x :: xs)).prod * if 0 < (x :: xs).length then a else 1) * (drop (0 + 1) (x :: xs)).prod

Tactic:
simp [set]

Result:
no goals

Proof state:
M : Type u_4
inst✝ : Monoid M
x✝¹ : ℕ
x✝ : M
⊢ ([].set x✝¹ x✝).prod = ((take x✝¹ []).prod * if x✝¹ < [].length then x✝ else 1) * (drop (x✝¹ + 1) []).prod

Tactic:
simp [set, (Nat.zero_le _).not_lt, Nat.zero_le]

Result:
no goals

Proof state:
M : Type u_4
inst✝ : Monoid M
x : M
xs : List M
i : ℕ
a : M
⊢ ((x :: xs).set (i + 1) a).prod =
    ((take (i + 1) (x :: xs)).prod * if i + 1 < (x :: xs).length then a else 1) * (drop (i + 1 + 1) (x :: xs)).prod

Tactic:
simp [set, prod_set xs i a, mul_assoc, Nat.add_lt_add_iff_right]

Result:
no goals
-- Mathlib/GroupTheory/Congruence/Hom.lean
theorem lift_funext (f g : c.Quotient →* P) (h : ∀ a : M, f a = g a) : f = g

Proof state:
case e_f
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f g : c.Quotient →* P
h : ∀ (a : M), f ↑a = g ↑a
⊢ f.comp c.mk' = g.comp c.mk'

Tactic:
exact DFunLike.ext_iff.2 h

Result:
no goals

Proof state:
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f g : c.Quotient →* P
h : ∀ (a : M), f ↑a = g ↑a
⊢ f = g

Tactic:
rw [← lift_apply_mk' f, ← lift_apply_mk' g]

Result:
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f g : c.Quotient →* P
h : ∀ (a : M), f ↑a = g ↑a
⊢ c.lift (f.comp c.mk') ⋯ = c.lift (g.comp c.mk') ⋯

Proof state:
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f g : c.Quotient →* P
h : ∀ (a : M), f ↑a = g ↑a
⊢ c.lift (f.comp c.mk') ⋯ = c.lift (g.comp c.mk') ⋯

Tactic:
congr 1

Result:
case e_f
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f g : c.Quotient →* P
h : ∀ (a : M), f ↑a = g ↑a
⊢ f.comp c.mk' = g.comp c.mk'
-- Mathlib/Data/Set/Function.lean
theorem injOn_insert {f : α → β} {s : Set α} {a : α} (has : a ∉ s) :
    Set.InjOn f (insert a s) ↔ Set.InjOn f s ∧ f a ∉ f '' s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
a : α
has : a ∉ s
⊢ (InjOn f s ∧ InjOn f {a} ∧ ∀ x ∈ s, ∀ y ∈ {a}, f x ≠ f y) ↔ InjOn f s ∧ f a ∉ f '' s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
a : α
has : a ∉ s
⊢ InjOn f (insert a s) ↔ InjOn f s ∧ f a ∉ f '' s

Tactic:
rw [← union_singleton, injOn_union (disjoint_singleton_right.2 has)]

Result:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
a : α
has : a ∉ s
⊢ (InjOn f s ∧ InjOn f {a} ∧ ∀ x ∈ s, ∀ y ∈ {a}, f x ≠ f y) ↔ InjOn f s ∧ f a ∉ f '' s
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
lemma map_inverseImage_eq_of_isEquivalence
    (P : MorphismProperty D) [P.RespectsIso] (F : C ⥤ D) [F.IsEquivalence] :
    (P.inverseImage F).map F = P

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u_1
inst✝² : Category.{u_2, u_1} D
P : MorphismProperty D
inst✝¹ : P.RespectsIso
F : C ⥤ D
inst✝ : F.IsEquivalence
⊢ (P.inverseImage F).map F = P

Tactic:
erw [P.inverseImage_equivalence_inverse_eq_map_functor F.asEquivalence, map_map,
  P.map_eq_of_iso F.asEquivalence.counitIso, map_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x)

Proof state:
x y : Nat
⊢ x.succ.gcd y = (y % x.succ).gcd x.succ

Tactic:
rw [gcd]

Result:
x y : Nat
⊢ (if x.succ = 0 then y else (y % x.succ).gcd x.succ) = (y % x.succ).gcd x.succ

Proof state:
x y : Nat
⊢ (if x.succ = 0 then y else (y % x.succ).gcd x.succ) = (y % x.succ).gcd x.succ

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/PFunctor/Multivariate/Basic.lean
theorem const.mk_get (x : const n A α) : const.mk n (const.get x) = x

Proof state:
case mk
n : ℕ
A : Type u
α : TypeVec.{u} n
fst✝ : (const n A).A
snd✝ : (const n A).B fst✝ ⟹ α
⊢ mk n (get ⟨fst✝, snd✝⟩) = ⟨fst✝, snd✝⟩

Tactic:
dsimp [const.get, const.mk]

Result:
case mk
n : ℕ
A : Type u
α : TypeVec.{u} n
fst✝ : (const n A).A
snd✝ : (const n A).B fst✝ ⟹ α
⊢ ⟨fst✝, fun x a => PEmpty.elim a⟩ = ⟨fst✝, snd✝⟩

Proof state:
case mk
n : ℕ
A : Type u
α : TypeVec.{u} n
fst✝ : (const n A).A
snd✝ : (const n A).B fst✝ ⟹ α
⊢ ⟨fst✝, fun x a => PEmpty.elim a⟩ = ⟨fst✝, snd✝⟩

Tactic:
congr with (_⟨⟩)

Result:
no goals

Proof state:
n : ℕ
A : Type u
α : TypeVec.{u} n
x : ↑(const n A) α
⊢ mk n (get x) = x

Tactic:
cases x

Result:
case mk
n : ℕ
A : Type u
α : TypeVec.{u} n
fst✝ : (const n A).A
snd✝ : (const n A).B fst✝ ⟹ α
⊢ mk n (get ⟨fst✝, snd✝⟩) = ⟨fst✝, snd✝⟩
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_udiv : eval .udiv = ((· / ·) : BitVec w → BitVec w → BitVec w)

Proof state:
w : Nat
⊢ udiv.eval = fun x1 x2 => x1 / x2

Tactic:
rfl

Result:
no goals
-- Mathlib/FieldTheory/Normal/Basic.lean
theorem exists_algEquiv_of_root [Normal K L] {x y : L} (hy : IsAlgebraic K y)
    (h_ev : (Polynomial.aeval x) (minpoly K y) = 0) : ∃ σ : L ≃ₐ[K] L, σ x = y

Proof state:
K : Type u_6
L : Type u_7
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : (Polynomial.aeval x) (minpoly K y) = 0
hx : IsAlgebraic K x
f : ↥K⟮x⟯ ≃ₐ[K] ↥K⟮y⟯ := algEquiv hx ⋯
hxy : (f.liftNormal L) ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)) = y
⊢ ∃ σ, σ x = y

Tactic:
exact ⟨(liftNormal f L), hxy⟩

Result:
no goals

Proof state:
K : Type u_6
L : Type u_7
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : (Polynomial.aeval x) (minpoly K y) = 0
hx : IsAlgebraic K x
⊢ ∃ σ, σ x = y

Tactic:
set f : K⟮x⟯ ≃ₐ[K] K⟮y⟯ := algEquiv hx (eq_of_root hy h_ev)

Result:
K : Type u_6
L : Type u_7
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : (Polynomial.aeval x) (minpoly K y) = 0
hx : IsAlgebraic K x
f : ↥K⟮x⟯ ≃ₐ[K] ↥K⟮y⟯ := algEquiv hx ⋯
⊢ ∃ σ, σ x = y

Proof state:
K : Type u_6
L : Type u_7
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : (Polynomial.aeval x) (minpoly K y) = 0
⊢ ∃ σ, σ x = y

Tactic:
have hx : IsAlgebraic K x := ⟨minpoly K y, ne_zero hy.isIntegral, h_ev⟩

Result:
K : Type u_6
L : Type u_7
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : (Polynomial.aeval x) (minpoly K y) = 0
hx : IsAlgebraic K x
⊢ ∃ σ, σ x = y

Proof state:
K : Type u_6
L : Type u_7
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : (Polynomial.aeval x) (minpoly K y) = 0
hx : IsAlgebraic K x
f : ↥K⟮x⟯ ≃ₐ[K] ↥K⟮y⟯ := algEquiv hx ⋯
⊢ ∃ σ, σ x = y

Tactic:
have hxy : (liftNormal f L) ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)) = y := by
  rw [liftNormal_commutes f L, algEquiv_apply, AdjoinSimple.algebraMap_gen K y]

Result:
K : Type u_6
L : Type u_7
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : (Polynomial.aeval x) (minpoly K y) = 0
hx : IsAlgebraic K x
f : ↥K⟮x⟯ ≃ₐ[K] ↥K⟮y⟯ := algEquiv hx ⋯
hxy : (f.liftNormal L) ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)) = y
⊢ ∃ σ, σ x = y

Proof state:
K : Type u_6
L : Type u_7
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : (Polynomial.aeval x) (minpoly K y) = 0
hx : IsAlgebraic K x
f : ↥K⟮x⟯ ≃ₐ[K] ↥K⟮y⟯ := algEquiv hx ⋯
⊢ (f.liftNormal L) ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)) = y

Tactic:
rw [liftNormal_commutes f L, algEquiv_apply, AdjoinSimple.algebraMap_gen K y]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem single_embedding {n : ℕ} (h : 0 < n) (i : Fin n) :
    ((single n h).embedding (0 : Fin 1)) i = i

Proof state:
n : ℕ
h : 0 < n
i : Fin n
⊢ ((single n h).embedding 0) i = i

Tactic:
ext

Result:
case h
n : ℕ
h : 0 < n
i : Fin n
⊢ ↑(((single n h).embedding 0) i) = ↑i

Proof state:
case h
n : ℕ
h : 0 < n
i : Fin n
⊢ ↑(((single n h).embedding 0) i) = ↑i

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addZ_of_Z_eq_zero_left [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P)
    (hPz : P z = 0) : W'.addZ P Q = P y ^ 2 * Q z * Q z

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.addZ P Q = P y ^ 2 * Q z * Q z

Tactic:
rw [addZ, hPz, X_eq_zero_of_Z_eq_zero hP hPz]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -3 * 0 ^ 2 * Q x * Q z + 3 * 0 * Q x ^ 2 * 0 + P y ^ 2 * Q z ^ 2 - Q y ^ 2 * 0 ^ 2 + W'.a₁ * 0 * P y * Q z ^ 2 -
                  W'.a₁ * Q x * Q y * 0 ^ 2 -
                W'.a₂ * 0 ^ 2 * Q z ^ 2 +
              W'.a₂ * Q x ^ 2 * 0 ^ 2 +
            W'.a₃ * P y * 0 * Q z ^ 2 -
          W'.a₃ * Q y * 0 ^ 2 * Q z -
        W'.a₄ * 0 * 0 * Q z ^ 2 +
      W'.a₄ * Q x * 0 ^ 2 * Q z =
    P y ^ 2 * Q z * Q z

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -3 * 0 ^ 2 * Q x * Q z + 3 * 0 * Q x ^ 2 * 0 + P y ^ 2 * Q z ^ 2 - Q y ^ 2 * 0 ^ 2 + W'.a₁ * 0 * P y * Q z ^ 2 -
                  W'.a₁ * Q x * Q y * 0 ^ 2 -
                W'.a₂ * 0 ^ 2 * Q z ^ 2 +
              W'.a₂ * Q x ^ 2 * 0 ^ 2 +
            W'.a₃ * P y * 0 * Q z ^ 2 -
          W'.a₃ * Q y * 0 ^ 2 * Q z -
        W'.a₄ * 0 * 0 * Q z ^ 2 +
      W'.a₄ * Q x * 0 ^ 2 * Q z =
    P y ^ 2 * Q z * Q z

Tactic:
ring1

Result:
no goals