harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
theorem ratAdd_sound {n : Nat} (f : DefaultFormula n) (c : DefaultClause n)
    (pivot : Literal (PosFin n)) (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat))
    (f' : DefaultFormula n) (f_readyForRatAdd : ReadyForRatAdd f) (pivot_in_c : pivot ∈ Clause.toList c)
    (ratAddSuccess : performRatAdd f c pivot rupHints ratHints = (f', true)) :
    Equisat (PosFin n) f f'

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
pivot : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.ReadyForRatAdd
pivot_in_c : pivot ∈ Clause.toList c
f'_def : f' = f.insert c
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
ratAddSuccess :
  ({
              clauses :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).1.clauses,
              rupUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).1.rupUnits,
              ratUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).1.ratUnits,
              assignments :=
                restoreAssignments
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).snd =
    true
⊢ Equisat (PosFin n) f (f.insert c)

Tactic:
exact safe_insert_of_performRatCheck_fold_success f f_readyForRatAdd c pivot rupHints ratHints pivot_in_c
  ratHintsExhaustive_eq_true performRatCheck_fold_success

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem X_pow_eq (s : σ) (n : ℕ) : (X s : MvPowerSeries σ R) ^ n = monomial R (single s n) 1

Proof state:
case succ
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
ih : X s ^ n = (monomial R (single s n)) 1
⊢ X s ^ (n + 1) = (monomial R (single s (n + 1))) 1

Tactic:
rw [pow_succ, ih, Finsupp.single_add, X, monomial_mul_monomial, one_mul]

Result:
no goals

Proof state:
case zero
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
⊢ X s ^ 0 = (monomial R (single s 0)) 1

Tactic:
simp

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
⊢ X s ^ n = (monomial R (single s n)) 1

Tactic:
induction n with
| zero => simp
| succ n ih => rw [pow_succ, ih, Finsupp.single_add, X, monomial_mul_monomial, one_mul]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Card.lean
@[to_additive]
lemma natCard_div_le : Nat.card (s / t) ≤ Nat.card s * Nat.card t

Proof state:
G : Type u_1
inst✝ : Group G
s t : Set G
⊢ Nat.card ↑(s * t⁻¹) ≤ Nat.card ↑s * Nat.card ↑t⁻¹

Tactic:
exact natCard_mul_le

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
s t : Set G
⊢ Nat.card ↑(s / t) ≤ Nat.card ↑s * Nat.card ↑t

Tactic:
rw [div_eq_mul_inv, ← natCard_inv t]

Result:
G : Type u_1
inst✝ : Group G
s t : Set G
⊢ Nat.card ↑(s * t⁻¹) ≤ Nat.card ↑s * Nat.card ↑t⁻¹
-- Mathlib/Probability/Distributions/Gamma.lean
lemma isProbabilityMeasureGamma {a r : ℝ} (ha : 0 < a) (hr : 0 < r) :
    IsProbabilityMeasure (gammaMeasure a r) where
  measure_univ

Proof state:
a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ (gammaMeasure a r) univ = 1

Tactic:
simp [gammaMeasure, lintegral_gammaPDF_eq_one ha hr]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma expGrowthInf_biInf {α : Type*} (u : α → ℕ → ℝ≥0∞) {s : Set α} (hs : s.Finite) :
    expGrowthInf (⨅ x ∈ s, u x) = ⨅ x ∈ s, expGrowthInf (u x)

Proof state:
α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Set α
hs : s.Finite
⊢ expGrowthInf (⨅ x ∈ s, u x) = ⨅ x ∈ s, expGrowthInf (u x)

Tactic:
have := map_finset_inf expGrowthInfTopHom hs.toFinset u

Result:
α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Set α
hs : s.Finite
this : expGrowthInfTopHom (hs.toFinset.inf u) = hs.toFinset.inf (⇑expGrowthInfTopHom ∘ u)
⊢ expGrowthInf (⨅ x ∈ s, u x) = ⨅ x ∈ s, expGrowthInf (u x)

Proof state:
α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Set α
hs : s.Finite
this : expGrowthInfTopHom (hs.toFinset.inf u) = hs.toFinset.inf (⇑expGrowthInfTopHom ∘ u)
⊢ expGrowthInf (⨅ x ∈ s, u x) = ⨅ x ∈ s, expGrowthInf (u x)

Tactic:
simpa only [expGrowthInfTopHom, InfTopHom.coe_mk, InfHom.coe_mk, Finset.inf_eq_iInf,
  hs.mem_toFinset, comp_apply]

Result:
no goals
-- Mathlib/Data/Nat/Hyperoperation.lean
theorem hyperoperation_ge_four_zero (n k : ℕ) :
    hyperoperation (n + 4) 0 k = if Even k then 1 else 0

Proof state:
case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 3) 0 (hyperoperation (n + 3 + 1) 0 kk) = if Even (kk + 1) then 1 else 0

Tactic:
rw [kih]

Result:
case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 3) 0 (if Even kk then 1 else 0) = if Even (kk + 1) then 1 else 0

Proof state:
case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 4) 0 (kk + 1) = if Even (kk + 1) then 1 else 0

Tactic:
rw [hyperoperation_recursion]

Result:
case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 3) 0 (hyperoperation (n + 3 + 1) 0 kk) = if Even (kk + 1) then 1 else 0

Proof state:
case zero
n : ℕ
⊢ hyperoperation (n + 4) 0 0 = if Even 0 then 1 else 0

Tactic:
rw [hyperoperation_ge_three_eq_one]

Result:
case zero
n : ℕ
⊢ 1 = if Even 0 then 1 else 0

Proof state:
case pos
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
h✝ : Even kk
⊢ hyperoperation (n + 3) 0 1 = 0

Tactic:
exact hyperoperation_ge_two_eq_self (n + 1) 0

Result:
no goals

Proof state:
case neg
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
h✝ : ¬Even kk
⊢ hyperoperation (n + 3) 0 0 = 1

Tactic:
exact hyperoperation_ge_three_eq_one n 0

Result:
no goals

Proof state:
n k : ℕ
⊢ hyperoperation (n + 4) 0 k = if Even k then 1 else 0

Tactic:
induction' k with kk kih

Result:
case zero
n : ℕ
⊢ hyperoperation (n + 4) 0 0 = if Even 0 then 1 else 0

case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 4) 0 (kk + 1) = if Even (kk + 1) then 1 else 0

Proof state:
case zero
n : ℕ
⊢ 1 = if Even 0 then 1 else 0

Tactic:
simp only [Even.zero, if_true]

Result:
no goals

Proof state:
case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 3) 0 (if Even kk then 1 else 0) = if ¬Even kk then 1 else 0

Tactic:
split_ifs

Result:
case pos
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
h✝ : Even kk
⊢ hyperoperation (n + 3) 0 1 = 0

case neg
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
h✝ : ¬Even kk
⊢ hyperoperation (n + 3) 0 0 = 1

Proof state:
case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 3) 0 (if Even kk then 1 else 0) = if Even (kk + 1) then 1 else 0

Tactic:
simp_rw [Nat.even_add_one]

Result:
case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 3) 0 (if Even kk then 1 else 0) = if ¬Even kk then 1 else 0
-- Mathlib/Data/Fin/Basic.lean
lemma predAbove_zero [NeZero n] {i : Fin (n + 1)} :
    predAbove (0 : Fin n) i = if hi : i = 0 then 0 else i.pred hi

Proof state:
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ predAbove 0 i = if hi : i = 0 then 0 else i.pred hi

Tactic:
split_ifs with hi

Result:
case pos
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
hi : i = 0
⊢ predAbove 0 i = 0

case neg
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
hi : ¬i = 0
⊢ predAbove 0 i = i.pred hi

Proof state:
case neg
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
hi : ¬i = 0
⊢ predAbove 0 i = i.pred hi

Tactic:
rw [predAbove_zero_of_ne_zero hi]

Result:
no goals

Proof state:
case pos
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
hi : i = 0
⊢ predAbove 0 i = 0

Tactic:
rw [hi, predAbove_right_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Swap.lean
@[simp]
lemma swap_mulVec_apply (i j : n) (a : n → R) :
    (swap R i j *ᵥ a) i = a j

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
a : n → R
⊢ (swap R i j *ᵥ a) i = a j

Tactic:
simp [swap, PEquiv.toMatrix_toPEquiv_mulVec]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem modify_eraseIdx_of_lt (f : α → α) (i j) (l : List α) (h : j < i) :
    (l.eraseIdx i).modify f j = (l.modify f j).eraseIdx i

Proof state:
case pos.isTrue.isTrue
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : j = k + 1
h✝¹ : j = k
h✝ : k < i
⊢ f l[k] = f l[k]

case pos.isTrue.isFalse
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : j = k + 1
h✝¹ : j = k
h✝ : ¬k < i
⊢ f l[k + 1] = f l[k + 1]

case pos.isFalse.isTrue
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : j = k + 1
h✝¹ : ¬j = k
h✝ : k < i
⊢ l[k] = l[k]

case pos.isFalse.isFalse
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : j = k + 1
h✝¹ : ¬j = k
h✝ : ¬k < i
⊢ l[k + 1] = f l[k + 1]

case neg.isTrue.isTrue
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : ¬j = k + 1
h✝¹ : j = k
h✝ : k < i
⊢ f l[k] = f l[k]

case neg.isTrue.isFalse
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : ¬j = k + 1
h✝¹ : j = k
h✝ : ¬k < i
⊢ f l[k + 1] = l[k + 1]

case neg.isFalse.isTrue
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : ¬j = k + 1
h✝¹ : ¬j = k
h✝ : k < i
⊢ l[k] = l[k]

case neg.isFalse.isFalse
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
h' : ¬j = k + 1
h✝¹ : ¬j = k
h✝ : ¬k < i
⊢ l[k + 1] = l[k + 1]

Tactic:
all_goals (first | rfl | omega)

Result:
no goals

Proof state:
case hl
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
⊢ (modify f j (l.eraseIdx i)).length = ((modify f j l).eraseIdx i).length

Tactic:
simp [length_eraseIdx]

Result:
no goals

Proof state:
case h
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
⊢ ∀ (i_1 : Nat) (h₁ : i_1 < (modify f j (l.eraseIdx i)).length) (h₂ : i_1 < ((modify f j l).eraseIdx i).length),
    (modify f j (l.eraseIdx i))[i_1] = ((modify f j l).eraseIdx i)[i_1]

Tactic:
intro k h₁ h₂

Result:
case h
α : Type u_1
f : α → α
i j : Nat
l : List α
h : j < i
k : Nat
h₁ : k < (modify f j (l.eraseIdx i)).length
h₂ : k < ((modify f j l).eraseIdx i).length
⊢ (modify f j (l.eraseIdx i))[k] = ((modify f j l).eraseIdx i)[k]
-- Mathlib/Topology/PartialHomeomorph.lean
theorem transPartialHomeomorph_trans (e : X ≃ₜ Y) (f : PartialHomeomorph Y Z)
    (f' : PartialHomeomorph Z Z') :
    (e.transPartialHomeomorph f).trans f' = e.transPartialHomeomorph (f.trans f')

Proof state:
X : Type u_1
Y : Type u_3
Z : Type u_5
Z' : Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : X ≃ₜ Y
f : PartialHomeomorph Y Z
f' : PartialHomeomorph Z Z'
⊢ (e.transPartialHomeomorph f).trans f' = e.transPartialHomeomorph (f.trans f')

Tactic:
simp only [transPartialHomeomorph_eq_trans, PartialHomeomorph.trans_assoc]

Result:
no goals
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem two_lt_q (p' : ℕ) : 2 < q (p' + 2)

Proof state:
case refine_1
p' : ℕ
⊢ 1 < p' + 2

Tactic:
exact le_add_left _ _

Result:
no goals

Proof state:
case refine_2
p' : ℕ
⊢ (mersenne (p' + 2)).minFac ≠ 2

Tactic:
rw [Ne, minFac_eq_two_iff, mersenne, Nat.pow_succ']

Result:
case refine_2
p' : ℕ
⊢ ¬2 ∣ 2 * 2 ^ (p' + 1) - 1

Proof state:
case refine_2
p' : ℕ
⊢ ¬2 ∣ 2 * 2 ^ (p' + 1) - 1

Tactic:
exact Nat.two_not_dvd_two_mul_sub_one Nat.one_le_two_pow

Result:
no goals

Proof state:
p' : ℕ
⊢ 2 < q (p' + 2)

Tactic:
refine (minFac_prime (one_lt_mersenne.2 ?_).ne').two_le.lt_of_ne' ?_

Result:
case refine_1
p' : ℕ
⊢ 1 < p' + 2

case refine_2
p' : ℕ
⊢ (mersenne (p' + 2)).minFac ≠ 2
-- Mathlib/Data/Matroid/Closure.lean
lemma isBasis'_iff_isBasis_closure : M.IsBasis' I X ↔ M.IsBasis I (M.closure X) ∧ I ⊆ X

Proof state:
α : Type u_2
M : Matroid α
X I : Set α
⊢ M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I (M.closure (X ∩ M.E)) ∧ I ⊆ X

Tactic:
exact ⟨fun h ↦ ⟨h.isBasis_closure_right, h.subset.trans inter_subset_left⟩,
  fun h ↦ h.1.isBasis_subset (subset_inter h.2 h.1.indep.subset_ground) (M.subset_closure _)⟩

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
X I : Set α
⊢ M.IsBasis' I X ↔ M.IsBasis I (M.closure X) ∧ I ⊆ X

Tactic:
rw [← closure_inter_ground, isBasis'_iff_isBasis_inter_ground]

Result:
α : Type u_2
M : Matroid α
X I : Set α
⊢ M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I (M.closure (X ∩ M.E)) ∧ I ⊆ X
-- Mathlib/Order/Disjoint.lean
theorem disjoint_sup_right : Disjoint a (b ⊔ c) ↔ Disjoint a b ∧ Disjoint a c

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b c : α
⊢ Disjoint a (b ⊔ c) ↔ Disjoint a b ∧ Disjoint a c

Tactic:
simp only [disjoint_iff, inf_sup_left, sup_eq_bot_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_replaceEntry_of_false [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
    {k a : α} {v : β} (h : (k == a) = false) :
    getValue? a (replaceEntry k v l) = getValue? a l

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
v : β
h : (k == a) = false
⊢ getValue? a (replaceEntry k v l) = getValue? a l

Tactic:
simp [getValue?_eq_getEntry?, getEntry?_replaceEntry_of_false h]

Result:
no goals
-- Mathlib/Tactic/NormNum/Result.lean
theorem IsRat.to_isInt {α} [Ring α] : ∀ {a : α} {n}, IsRat a n (nat_lit 1) → IsInt a n
  | _, _, ⟨inv, rfl⟩ => have := @invertibleOne α _; ⟨by simp⟩

Proof state:
α : Type u_1
inst✝ : Ring α
num✝ : ℤ
inv : Invertible ↑1
this : Invertible 1
⊢ ↑num✝ * ⅟↑1 = ↑num✝

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem concat_ne_nil {u v : V} (p : G.Walk u v) (h : G.Adj v u) : p.concat h ≠ nil

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : G.Adj v u
⊢ p.concat h ≠ nil

Tactic:
cases p <;> simp [concat]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean
theorem toBaseChange_comp_involute (Q : QuadraticForm R V) :
    (toBaseChange A Q).comp (involute : CliffordAlgebra (Q.baseChange A) →ₐ[A] _) =
      (Algebra.TensorProduct.map (AlgHom.id _ _) involute).comp (toBaseChange A Q)

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
⊢ (toBaseChange A Q).comp involute = (Algebra.TensorProduct.map (AlgHom.id A A) involute).comp (toBaseChange A Q)

Tactic:
ext v

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
v : V
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (((toBaseChange A Q).comp involute).toLinearMap ∘ₗ ι (QuadraticForm.baseChange A Q)))
        1)
      v =
    ((TensorProduct.AlgebraTensorModule.curry
          (((Algebra.TensorProduct.map (AlgHom.id A A) involute).comp (toBaseChange A Q)).toLinearMap ∘ₗ
            ι (QuadraticForm.baseChange A Q)))
        1)
      v

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
v : V
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (((toBaseChange A Q).comp involute).toLinearMap ∘ₗ ι (QuadraticForm.baseChange A Q)))
        1)
      v =
    ((TensorProduct.AlgebraTensorModule.curry
          (((Algebra.TensorProduct.map (AlgHom.id A A) involute).comp (toBaseChange A Q)).toLinearMap ∘ₗ
            ι (QuadraticForm.baseChange A Q)))
        1)
      v

Tactic:
show toBaseChange A Q (involute (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))
  = (Algebra.TensorProduct.map (AlgHom.id _ _) involute :
      A ⊗[R] CliffordAlgebra Q →ₐ[A] _)
    (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))

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
v : V
⊢ (toBaseChange A Q) (involute ((ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v))) =
    (Algebra.TensorProduct.map (AlgHom.id A A) involute)
      ((toBaseChange A Q) ((ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v)))

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
v : V
⊢ (toBaseChange A Q) (involute ((ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v))) =
    (Algebra.TensorProduct.map (AlgHom.id A A) involute)
      ((toBaseChange A Q) ((ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v)))

Tactic:
rw [toBaseChange_ι, involute_ι, map_neg (toBaseChange A Q), toBaseChange_ι,
  Algebra.TensorProduct.map_tmul, AlgHom.id_apply, involute_ι, TensorProduct.tmul_neg]

Result:
no goals
-- Mathlib/Data/ENNReal/Order.lean
theorem pow_eq_top_iff {n : ℕ} : a ^ n = ∞ ↔ a = ∞ ∧ n ≠ 0

Proof state:
case inl
a : ℝ≥0∞
⊢ a ^ 0 = ⊤ ↔ a = ⊤ ∧ 0 ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
case inr.top
a : ℝ≥0∞
n : ℕ
hn : 0 < n
⊢ ⊤ ^ n = ⊤ ↔ ⊤ = ⊤ ∧ n ≠ 0

Tactic:
simp only [Ne, hn.ne', top_pow hn, not_false_eq_true, and_self]

Result:
no goals

Proof state:
a : ℝ≥0∞
n : ℕ
⊢ a ^ n = ⊤ ↔ a = ⊤ ∧ n ≠ 0

Tactic:
rcases n.eq_zero_or_pos with rfl | (hn : 0 < n)

Result:
case inl
a : ℝ≥0∞
⊢ a ^ 0 = ⊤ ↔ a = ⊤ ∧ 0 ≠ 0

case inr
a : ℝ≥0∞
n : ℕ
hn : 0 < n
⊢ a ^ n = ⊤ ↔ a = ⊤ ∧ n ≠ 0

Proof state:
case inr.coe
a : ℝ≥0∞
n : ℕ
hn : 0 < n
x✝ : ℝ≥0
⊢ ↑x✝ ^ n = ⊤ ↔ ↑x✝ = ⊤ ∧ n ≠ 0

Tactic:
simp only [← coe_pow, coe_ne_top, false_and]

Result:
no goals

Proof state:
case inr
a : ℝ≥0∞
n : ℕ
hn : 0 < n
⊢ a ^ n = ⊤ ↔ a = ⊤ ∧ n ≠ 0

Tactic:
induction a

Result:
case inr.top
a : ℝ≥0∞
n : ℕ
hn : 0 < n
⊢ ⊤ ^ n = ⊤ ↔ ⊤ = ⊤ ∧ n ≠ 0

case inr.coe
a : ℝ≥0∞
n : ℕ
hn : 0 < n
x✝ : ℝ≥0
⊢ ↑x✝ ^ n = ⊤ ↔ ↑x✝ = ⊤ ∧ n ≠ 0
-- Mathlib/Algebra/Group/Subgroup/Map.lean
theorem map_symm_eq_iff_map_eq {H : Subgroup N} {e : G ≃* N} :
    H.map ↑e.symm = K ↔ K.map ↑e = H

Proof state:
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ map (↑e.symm) H = K ↔ map (↑e) K = H

Tactic:
constructor <;> rintro rfl

Result:
case mp
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ map (↑e) (map (↑e.symm) H) = H

case mpr
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
e : G ≃* N
⊢ map (↑e.symm) (map (↑e) K) = K

Proof state:
case mp
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup N
e : G ≃* N
⊢ map (↑e) (map (↑e.symm) H) = H

Tactic:
rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self,
  MulEquiv.coe_monoidHom_refl, map_id]

Result:
no goals

Proof state:
case mpr
G : Type u_1
inst✝¹ : Group G
K : Subgroup G
N : Type u_5
inst✝ : Group N
e : G ≃* N
⊢ map (↑e.symm) (map (↑e) K) = K

Tactic:
rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.self_trans_symm,
  MulEquiv.coe_monoidHom_refl, map_id]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsBigOWith.pow' {f : α → R} {g : α → 𝕜} (h : IsBigOWith c l f g) :
    ∀ n : ℕ, IsBigOWith (Nat.casesOn n ‖(1 : R)‖ fun n => c ^ (n + 1))
      l (fun x => f x ^ n) fun x => g x ^ n
  | 0 => by simpa using isBigOWith_const_const (1 : R) (one_ne_zero' 𝕜) l
  | 1 => by simpa
  | n + 2 => by simpa [pow_succ] using (IsBigOWith.pow' h (n + 1)).mul h

Proof state:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
f : α → R
g : α → 𝕜
h : IsBigOWith c l f g
⊢ IsBigOWith (Nat.casesOn 0 ‖1‖ fun n => c ^ (n + 1)) l (fun x => f x ^ 0) fun x => g x ^ 0

Tactic:
simpa using isBigOWith_const_const (1 : R) (one_ne_zero' 𝕜) l

Result:
no goals

Proof state:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
f : α → R
g : α → 𝕜
h : IsBigOWith c l f g
⊢ IsBigOWith (Nat.casesOn 1 ‖1‖ fun n => c ^ (n + 1)) l (fun x => f x ^ 1) fun x => g x ^ 1

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
f : α → R
g : α → 𝕜
h : IsBigOWith c l f g
n : ℕ
⊢ IsBigOWith (Nat.casesOn (n + 2) ‖1‖ fun n => c ^ (n + 1)) l (fun x => f x ^ (n + 2)) fun x => g x ^ (n + 2)

Tactic:
simpa [pow_succ] using (IsBigOWith.pow' h (n + 1)).mul h

Result:
no goals
-- Mathlib/Logic/IsEmpty.lean
theorem rightTotal_empty [IsEmpty β] : RightTotal R

Proof state:
α : Type u_4
β : Type u_5
R : α → β → Prop
inst✝ : IsEmpty β
⊢ RightTotal R

Tactic:
simp only [RightTotal, IsEmpty.forall_iff]

Result:
no goals