harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Irreducible.lean
theorem isPreirreducible_iff_isClosed_union_isClosed :
    IsPreirreducible s ↔
      ∀ z₁ z₂ : Set X, IsClosed z₁ → IsClosed z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s z₁ z₂ : Set X
x✝¹ : IsClosed z₁
x✝ : IsClosed z₂
⊢ ¬s ⊆ z₁ → ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂

Tactic:
rw [← and_imp, ← not_or, not_imp_not]

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s z₁ z₂ : Set X
⊢ IsOpen z₁ᶜ → IsOpen z₂ᶜ → (s ∩ z₁ᶜ).Nonempty → (s ∩ z₂ᶜ).Nonempty → (s ∩ (z₁ᶜ ∩ z₂ᶜ)).Nonempty ↔
    IsClosed z₁ → IsClosed z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂

Tactic:
simp only [isOpen_compl_iff, ← compl_union, inter_compl_nonempty_iff]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s z₁ z₂ : Set X
⊢ IsClosed z₁ → IsClosed z₂ → ¬s ⊆ z₁ → ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔
    IsClosed z₁ → IsClosed z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s z₁ z₂ : Set X
⊢ IsClosed z₁ → IsClosed z₂ → ¬s ⊆ z₁ → ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔
    IsClosed z₁ → IsClosed z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂

Tactic:
refine forall₂_congr fun _ _ => ?_

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s z₁ z₂ : Set X
x✝¹ : IsClosed z₁
x✝ : IsClosed z₂
⊢ ¬s ⊆ z₁ → ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsPreirreducible s ↔ ∀ (z₁ z₂ : Set X), IsClosed z₁ → IsClosed z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂

Tactic:
refine compl_surjective.forall.trans <| forall_congr' fun z₁ => compl_surjective.forall.trans <|
  forall_congr' fun z₂ => ?_

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s z₁ z₂ : Set X
⊢ IsOpen z₁ᶜ → IsOpen z₂ᶜ → (s ∩ z₁ᶜ).Nonempty → (s ∩ z₂ᶜ).Nonempty → (s ∩ (z₁ᶜ ∩ z₂ᶜ)).Nonempty ↔
    IsClosed z₁ → IsClosed z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
-- Mathlib/GroupTheory/GroupAction/Quotient.lean
theorem Quotient.mk_smul_out [QuotientAction β H] (b : β) (q : α ⧸ H) :
    QuotientGroup.mk (b • q.out) = b • q

Proof state:
α : Type u
β : Type v
inst✝³ : Group α
inst✝² : Monoid β
inst✝¹ : MulAction β α
H : Subgroup α
inst✝ : QuotientAction β H
b : β
q : α ⧸ H
⊢ ↑(b • Quotient.out q) = b • q

Tactic:
rw [← Quotient.smul_mk, QuotientGroup.out_eq']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_insertMany_list_of_mem [LawfulBEq α] (h : m.1.WF)
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} [Inhabited (β k')]
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l) :
    (m.insertMany l).1.get! k' = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ (m.insertMany l).val.get! k' = cast ⋯ v

Tactic:
simp_to_model [insertMany] using List.getValueCast!_insertList_of_mem

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Proof state:
case e_a
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem coe_toNNReal_le_self : ∀ {a : ℝ≥0∞}, ↑a.toNNReal ≤ a
  | ofNNReal r => by rw [toNNReal_coe]
  | ⊤ => le_top

Proof state:
r : ℝ≥0
⊢ ↑(↑r).toNNReal ≤ ↑r

Tactic:
rw [toNNReal_coe]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Basic.lean
lemma not_mem_range_embeddingUpIntLE_iff (n : ℤ) :
    (∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n) ↔ p < n

Proof state:
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n
this : ¬p < n
⊢ p - ↑(p - n).natAbs = n

Tactic:
omega

Result:
no goals

Proof state:
case mpr
p n : ℤ
a✝ : p < n
i✝ : ℕ
⊢ (embeddingUpIntLE p).f i✝ ≠ n

Tactic:
dsimp

Result:
case mpr
p n : ℤ
a✝ : p < n
i✝ : ℕ
⊢ ¬p - ↑i✝ = n

Proof state:
case mpr
p n : ℤ
⊢ p < n → ∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n

Tactic:
intros

Result:
case mpr
p n : ℤ
a✝ : p < n
i✝ : ℕ
⊢ (embeddingUpIntLE p).f i✝ ≠ n

Proof state:
case mpr
p n : ℤ
a✝ : p < n
i✝ : ℕ
⊢ ¬p - ↑i✝ = n

Tactic:
omega

Result:
no goals

Proof state:
case mp
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n
⊢ p < n

Tactic:
by_contra!

Result:
case mp
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n
this : ¬p < n
⊢ False

Proof state:
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n
this : ¬p < n
⊢ (embeddingUpIntLE p).f (p - n).natAbs = n

Tactic:
simp

Result:
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n
this : ¬p < n
⊢ p - ↑(p - n).natAbs = n

Proof state:
case mp
p n : ℤ
⊢ (∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n) → p < n

Tactic:
intro h

Result:
case mp
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n
⊢ p < n

Proof state:
p n : ℤ
⊢ (∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n) ↔ p < n

Tactic:
constructor

Result:
case mp
p n : ℤ
⊢ (∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n) → p < n

case mpr
p n : ℤ
⊢ p < n → ∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n

Proof state:
case mp
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n
this : ¬p < n
⊢ False

Tactic:
exact h (p - n).natAbs (by simp; omega)

Result:
no goals
-- Mathlib/Topology/Path.lean
theorem refl_trans_refl {a : X} :
    (Path.refl a).trans (Path.refl a) = Path.refl a

Proof state:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
a : X
x✝ : ↑I
⊢ ((refl a).trans (refl a)) x✝ = (refl a) x✝

Tactic:
simp only [Path.trans, ite_self, one_div, Path.refl_extend]

Result:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
a : X
x✝ : ↑I
⊢ { toFun := (fun t => a) ∘ Subtype.val, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } x✝ = (refl a) x✝

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
a : X
⊢ (refl a).trans (refl a) = refl a

Tactic:
ext

Result:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
a : X
x✝ : ↑I
⊢ ((refl a).trans (refl a)) x✝ = (refl a) x✝

Proof state:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
a : X
x✝ : ↑I
⊢ { toFun := (fun t => a) ∘ Subtype.val, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } x✝ = (refl a) x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Convex/Star.lean
theorem StarConvex.add_smul_mem (hs : StarConvex 𝕜 x s) (hy : x + y ∈ s) {t : 𝕜} (ht₀ : 0 ≤ t)
    (ht₁ : t ≤ 1) : x + t • y ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : x + y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
⊢ x + t • y ∈ s

Tactic:
have h : x + t • y = (1 - t) • x + t • (x + y) := by
  rw [smul_add, ← add_assoc, ← add_smul, sub_add_cancel, one_smul]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : x + y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ x + t • y ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : x + y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ x + t • y ∈ s

Tactic:
rw [h]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : x + y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ (1 - t) • x + t • (x + y) ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : x + y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
⊢ x + t • y = (1 - t) • x + t • (x + y)

Tactic:
rw [smul_add, ← add_assoc, ← add_smul, sub_add_cancel, one_smul]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : x + y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ (1 - t) • x + t • (x + y) ∈ s

Tactic:
exact hs hy (sub_nonneg_of_le ht₁) ht₀ (sub_add_cancel _ _)

Result:
no goals
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
lemma quasispectrum_inr_eq (R S : Type*) {A : Type*} [Semifield R]
    [Field S] [NonUnitalRing A] [Algebra R S] [Module S A] [IsScalarTower S A A]
    [SMulCommClass S A A] [Module R A] [IsScalarTower R S A] (a : A) :
    quasispectrum R (a : Unitization S A) = quasispectrum R a

Proof state:
case h
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
⊢ {0} ⊆ spectrum R ↑a

Tactic:
simpa using zero_mem_spectrum_inr _ _ _

Result:
no goals

Proof state:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
⊢ spectrum R ↑a ∪ {0} = spectrum R ↑a

Tactic:
apply Set.union_eq_self_of_subset_right

Result:
case h
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
⊢ {0} ⊆ spectrum R ↑a

Proof state:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
⊢ quasispectrum R ↑a = quasispectrum R a

Tactic:
rw [quasispectrum_eq_spectrum_union_zero, quasispectrum_eq_spectrum_inr' R S]

Result:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
⊢ spectrum R ↑a ∪ {0} = spectrum R ↑a
-- Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
theorem χ₈'_int_eq_if_mod_eight (n : ℤ) :
    χ₈' n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1

Proof state:
n : ℤ
⊢ χ₈' ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1

Tactic:
have help :
  ∀ m : ℤ, 0 ≤ m → m < 8 → χ₈' m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1 := by
  decide

Result:
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈' ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1
⊢ χ₈' ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1

Proof state:
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈' ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1
⊢ χ₈' ↑(n % ↑8) = if n % 8 % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1

Tactic:
exact help (n % 8) (Int.emod_nonneg n (by omega)) (Int.emod_lt n (by omega))

Result:
no goals

Proof state:
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈' ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1
⊢ χ₈' ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1

Tactic:
rw [← Int.emod_emod_of_dvd n (by omega : (2 : ℤ) ∣ 8), ← ZMod.intCast_mod n 8]

Result:
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈' ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1
⊢ χ₈' ↑(n % ↑8) = if n % 8 % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1

Proof state:
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈' ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1
⊢ 2 ∣ 8

Tactic:
omega

Result:
no goals

Proof state:
n : ℤ
⊢ ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈' ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1

Tactic:
decide

Result:
no goals

Proof state:
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈' ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1
⊢ 8 ≠ 0

Tactic:
omega

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₂_of_isCharThreeJNeZeroNF_of_char_three : W.b₂ = W.a₂

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ W.b₂ = W.a₂

Tactic:
rw [b₂_of_isCharThreeJNeZeroNF]

Result:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ 4 * W.a₂ = W.a₂

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ 4 * W.a₂ = W.a₂

Tactic:
linear_combination W.a₂ * CharP.cast_eq_zero R 3

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
theorem LinearIndepOn.image_of_comp (f : ι → ι') (g : ι' → M) (hs : LinearIndepOn R (g ∘ f) s) :
    LinearIndepOn R g (f '' s)

Proof state:
ι : Type u'
ι' : Type u_1
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ι → ι'
g : ι' → M
hs : LinearIndepOn R (g ∘ f) s
⊢ LinearIndepOn R g (f '' s)

Tactic:
nontriviality R

Result:
ι : Type u'
ι' : Type u_1
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ι → ι'
g : ι' → M
hs : LinearIndepOn R (g ∘ f) s
a✝ : Nontrivial R
⊢ LinearIndepOn R g (f '' s)

Proof state:
ι : Type u'
ι' : Type u_1
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ι → ι'
g : ι' → M
hs : LinearIndepOn R (g ∘ f) s
a✝ : Nontrivial R
this : InjOn f s
⊢ LinearIndepOn R g (f '' s)

Tactic:
exact (linearIndependent_equiv' (Equiv.Set.imageOfInjOn f s this) rfl).1 hs

Result:
no goals

Proof state:
ι : Type u'
ι' : Type u_1
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ι → ι'
g : ι' → M
hs : LinearIndepOn R (g ∘ f) s
a✝ : Nontrivial R
⊢ LinearIndepOn R g (f '' s)

Tactic:
have : InjOn f s := injOn_iff_injective.2 hs.injective.of_comp

Result:
ι : Type u'
ι' : Type u_1
R : Type u_2
s : Set ι
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ι → ι'
g : ι' → M
hs : LinearIndepOn R (g ∘ f) s
a✝ : Nontrivial R
this : InjOn f s
⊢ LinearIndepOn R g (f '' s)
-- Mathlib/Data/Multiset/Powerset.lean
theorem powersetCardAux_perm {n} {l₁ l₂ : List α} (p : l₁ ~ l₂) :
    powersetCardAux n l₁ ~ powersetCardAux n l₂

Proof state:
case succ.swap
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
a b : α
l✝ : List α
⊢ powersetCardAux (n + 1) l✝ ++
      (List.map (cons a) (powersetCardAux n l✝) ++ List.map (cons b) (powersetCardAux n (a :: l✝))) ~
    powersetCardAux (n + 1) l✝ ++
      (List.map (cons b) (powersetCardAux n l✝) ++ List.map (cons a) (powersetCardAux n (b :: l✝)))

Tactic:
apply Perm.append_left

Result:
case succ.swap.a
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
a b : α
l✝ : List α
⊢ List.map (cons a) (powersetCardAux n l✝) ++ List.map (cons b) (powersetCardAux n (a :: l✝)) ~
    List.map (cons b) (powersetCardAux n l✝) ++ List.map (cons a) (powersetCardAux n (b :: l✝))

Proof state:
case succ.nil
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
⊢ powersetCardAux (n + 1) [] ~ powersetCardAux (n + 1) []

Tactic:
rfl

Result:
no goals

Proof state:
case succ.swap
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
a b : α
l✝ : List α
⊢ powersetCardAux (n + 1) (b :: a :: l✝) ~ powersetCardAux (n + 1) (a :: b :: l✝)

Tactic:
simp only [powersetCardAux_cons, append_assoc]

Result:
case succ.swap
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
a b : α
l✝ : List α
⊢ powersetCardAux (n + 1) l✝ ++
      (List.map (cons a) (powersetCardAux n l✝) ++ List.map (cons b) (powersetCardAux n (a :: l✝))) ~
    powersetCardAux (n + 1) l✝ ++
      (List.map (cons b) (powersetCardAux n l✝) ++ List.map (cons a) (powersetCardAux n (b :: l✝)))
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
private lemma toAffine_addX_of_ne {P Q : Fin 3 → F} (hPz : P z ≠ 0) (hQz : Q z ≠ 0) {n d : F}
    (hd : d ≠ 0) : W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (n / (P z * Q z * d)) =
      (n ^ 2 + W.a₁ * n * P z * Q z * d - W.a₂ * P z ^ 2 * Q z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2
        - Q x * P z ^ 2 * d ^ 2) / (P z * Q z) ^ 2 / d ^ 2

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ (toAffine W).addX (P x / P z ^ 2) (Q x / Q z ^ 2) (n / (P z * Q z * d)) =
    (n ^ 2 + W.a₁ * n * P z * Q z * d - W.a₂ * P z ^ 2 * Q z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2 -
          Q x * P z ^ 2 * d ^ 2) /
        (P z * Q z) ^ 2 /
      d ^ 2

Tactic:
field_simp [mul_ne_zero (mul_ne_zero hPz hQz) hd]

Result:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ (((n ^ 2 * (P z * Q z * d) + (toAffine W).a₁ * n * (P z * Q z * d) ^ 2 -
                (P z * Q z * d) ^ 2 * (P z * Q z * d) * (toAffine W).a₂) *
              P z ^ 2 -
            (P z * Q z * d) ^ 2 * (P z * Q z * d) * P x) *
          Q z ^ 2 -
        (P z * Q z * d) ^ 2 * (P z * Q z * d) * P z ^ 2 * Q x) *
      ((P z * Q z) ^ 2 * d ^ 2) =
    (n ^ 2 + W.a₁ * n * P z * Q z * d - W.a₂ * P z ^ 2 * Q z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2 -
        Q x * P z ^ 2 * d ^ 2) *
      ((P z * Q z * d) ^ 2 * (P z * Q z * d) * P z ^ 2 * Q z ^ 2)

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ (((n ^ 2 * (P z * Q z * d) + (toAffine W).a₁ * n * (P z * Q z * d) ^ 2 -
                (P z * Q z * d) ^ 2 * (P z * Q z * d) * (toAffine W).a₂) *
              P z ^ 2 -
            (P z * Q z * d) ^ 2 * (P z * Q z * d) * P x) *
          Q z ^ 2 -
        (P z * Q z * d) ^ 2 * (P z * Q z * d) * P z ^ 2 * Q x) *
      ((P z * Q z) ^ 2 * d ^ 2) =
    (n ^ 2 + W.a₁ * n * P z * Q z * d - W.a₂ * P z ^ 2 * Q z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2 -
        Q x * P z ^ 2 * d ^ 2) *
      ((P z * Q z * d) ^ 2 * (P z * Q z * d) * P z ^ 2 * Q z ^ 2)

Tactic:
ring1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} :
    ¬a ∈ m → get! m a = default

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.WF
a : α
⊢ ¬a ∈ m → get! m a = default

Tactic:
simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false h

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem smul_equiv_smul {G : Type*} [SMul G β] [IsScalarTower G β β] {f1 f2 : CauSeq β abv} (c : G)
    (hf : f1 ≈ f2) : c • f1 ≈ c • f2

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
G : Type u_3
inst✝¹ : SMul G β
inst✝ : IsScalarTower G β β
f1 f2 : CauSeq β abv
c : G
hf : f1 ≈ f2
⊢ c • f1 ≈ c • f2

Tactic:
simpa [const_smul, smul_one_mul _ _] using
  mul_equiv_mul (const_equiv.mpr <| Eq.refl <| c • (1 : β)) hf

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem mul_comm (x y : EReal) : x * y = y * x

Proof state:
case h_real.h_real
a✝¹ a✝ : ℝ
⊢ ↑a✝¹ * ↑a✝ = ↑a✝ * ↑a✝¹

Tactic:
rw [← coe_mul, ← coe_mul, mul_comm]

Result:
no goals

Proof state:
case h_top.h_top

⊢ ⊤ * ⊤ = ⊤ * ⊤

Tactic:
rfl

Result:
no goals

Proof state:
x y : EReal
⊢ x * y = y * x

Tactic:
induction x <;> induction y  <;>
  try { rfl }

Result:
case h_real.h_real
a✝¹ a✝ : ℝ
⊢ ↑a✝¹ * ↑a✝ = ↑a✝ * ↑a✝¹
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lex.lean
theorem lex_eq_false_iff_ge [DecidableEq α] [LT α] [DecidableLT α]
    {l₁ l₂ : Vector α n} : lex l₁ l₂ = false ↔ l₂ ≤ l₁

Proof state:
α : Type u_1
n : Nat
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₁ l₂ : Vector α n
⊢ (l₁.lex l₂ fun x1 x2 => decide (x1 < x2)) = false ↔ l₂ ≤ l₁

Tactic:
cases l₁

Result:
case mk
α : Type u_1
n : Nat
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₂ : Vector α n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.lex l₂ fun x1 x2 => decide (x1 < x2)) = false ↔
    l₂ ≤ { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk.mk
α : Type u_1
n : Nat
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.lex { toArray := toArray✝, size_toArray := size_toArray✝ }
        fun x1 x2 => decide (x1 < x2)) =
      false ↔
    { toArray := toArray✝, size_toArray := size_toArray✝ } ≤ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }

Tactic:
simp [Array.not_lt_iff_ge]

Result:
no goals

Proof state:
case mk
α : Type u_1
n : Nat
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₂ : Vector α n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.lex l₂ fun x1 x2 => decide (x1 < x2)) = false ↔
    l₂ ≤ { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
n : Nat
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.lex { toArray := toArray✝, size_toArray := size_toArray✝ }
        fun x1 x2 => decide (x1 < x2)) =
      false ↔
    { toArray := toArray✝, size_toArray := size_toArray✝ } ≤ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
/-- See also `Complex.cpow_int_mul'`. -/
lemma cpow_int_mul (x : ℂ) (n : ℤ) (y : ℂ) : x ^ (n * y) = (x ^ y) ^ n

Proof state:
case inl.inl
y : ℂ
⊢ 0 ^ (↑0 * y) = (0 ^ y) ^ 0

Tactic:
simp

Result:
no goals

Proof state:
x : ℂ
n : ℤ
y : ℂ
⊢ x ^ (↑n * y) = (x ^ y) ^ n

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Result:
case inl
n : ℤ
y : ℂ
⊢ 0 ^ (↑n * y) = (0 ^ y) ^ n

case inr
x : ℂ
n : ℤ
y : ℂ
hx : x ≠ 0
⊢ x ^ (↑n * y) = (x ^ y) ^ n

Proof state:
case inr
x : ℂ
n : ℤ
y : ℂ
hx : x ≠ 0
⊢ x ^ (↑n * y) = (x ^ y) ^ n

Tactic:
rw [cpow_def_of_ne_zero hx, cpow_def_of_ne_zero hx, mul_left_comm, exp_int_mul]

Result:
no goals

Proof state:
case inl
n : ℤ
y : ℂ
⊢ 0 ^ (↑n * y) = (0 ^ y) ^ n

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Result:
case inl.inl
y : ℂ
⊢ 0 ^ (↑0 * y) = (0 ^ y) ^ 0

case inl.inr
n : ℤ
y : ℂ
hn : n ≠ 0
⊢ 0 ^ (↑n * y) = (0 ^ y) ^ n

Proof state:
case inl.inr
n : ℤ
y : ℂ
hn : n ≠ 0
⊢ 0 ^ (↑n * y) = (0 ^ y) ^ n

Tactic:
rcases eq_or_ne y 0 with rfl | hy <;> simp [*, zero_zpow]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem equivMapDomain_refl' : equivMapDomain (Equiv.refl _) = @id (α →₀ M)

Proof state:
case h.h
α : Type u_1
M : Type u_5
inst✝ : Zero M
x : α →₀ M
a✝ : α
⊢ (equivMapDomain (Equiv.refl α) x) a✝ = (id x) a✝

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
⊢ equivMapDomain (Equiv.refl α) = id

Tactic:
ext x

Result:
case h.h
α : Type u_1
M : Type u_5
inst✝ : Zero M
x : α →₀ M
a✝ : α
⊢ (equivMapDomain (Equiv.refl α) x) a✝ = (id x) a✝