harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean
lemma isEmbedding_inducingFn [SeparatingDual 𝕜 F] : IsEmbedding (inducingFn 𝕜 E F)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜 F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : SeparatingDual 𝕜 F
A B : E →WOT[𝕜] F
hAB : (inducingFn 𝕜 E F) A = (inducingFn 𝕜 E F) B
⊢ ∀ (x : E) (y : F →L[𝕜] 𝕜), y (A x) = y (B x)

Tactic:
simpa [funext_iff] using hAB

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜 F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : SeparatingDual 𝕜 F
⊢ IsEmbedding ⇑(inducingFn 𝕜 E F)

Tactic:
refine Function.Injective.isEmbedding_induced fun A B hAB => ?_

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜 F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : SeparatingDual 𝕜 F
A B : E →WOT[𝕜] F
hAB : (inducingFn 𝕜 E F) A = (inducingFn 𝕜 E F) B
⊢ A = B

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜 F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : SeparatingDual 𝕜 F
A B : E →WOT[𝕜] F
hAB : (inducingFn 𝕜 E F) A = (inducingFn 𝕜 E F) B
⊢ A = B

Tactic:
rw [ContinuousLinearMapWOT.ext_dual_iff]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜 F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
inst✝ : SeparatingDual 𝕜 F
A B : E →WOT[𝕜] F
hAB : (inducingFn 𝕜 E F) A = (inducingFn 𝕜 E F) B
⊢ ∀ (x : E) (y : F →L[𝕜] 𝕜), y (A x) = y (B x)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Cooper.lean
theorem le_mul_resolve_left_inv (a p k : Int)
    (h₁ : 0 ≤ k) (h₄ : a ∣ k + p) :
    p ≤ a * resolve_left_inv a p k

Proof state:
a p k : Int
h₁ : 0 ≤ k
h₄ : a ∣ k + p
⊢ p ≤ k + p

Tactic:
apply Int.le_add_of_nonneg_left h₁

Result:
no goals

Proof state:
a p k : Int
h₁ : 0 ≤ k
h₄ : a ∣ k + p
⊢ p ≤ a * resolve_left_inv a p k

Tactic:
simp only [resolve_left_inv]

Result:
a p k : Int
h₁ : 0 ≤ k
h₄ : a ∣ k + p
⊢ p ≤ a * ((k + p) / a)

Proof state:
a p k : Int
h₁ : 0 ≤ k
h₄ : a ∣ k + p
⊢ p ≤ a * ((k + p) / a)

Tactic:
rw [Int.mul_ediv_cancel' h₄]

Result:
a p k : Int
h₁ : 0 ≤ k
h₄ : a ∣ k + p
⊢ p ≤ k + p
-- Mathlib/RingTheory/Kaehler/Basic.lean
theorem KaehlerDifferential.kerTotal_mkQ_single_add (x y z) : (z𝖣x + y) = (z𝖣x) + z𝖣y

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ (z𝖣x + y) = (z𝖣x) + z𝖣y

Tactic:
rw [← map_add, eq_comm, ← sub_eq_zero, ← map_sub (Submodule.mkQ (kerTotal R S)),
  Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ single x z + single y z - single (x + y) z ∈ kerTotal R S

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ z • (single x 1 + single y 1 - single (x + y) 1) ∈ kerTotal R S

Tactic:
exact Submodule.smul_mem _ _ (Submodule.subset_span (Or.inl <| Or.inl <| ⟨⟨_, _⟩, rfl⟩))

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ single x z + single y z - single (x + y) z ∈ kerTotal R S

Tactic:
simp_rw [← Finsupp.smul_single_one _ z, ← smul_add, ← smul_sub]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x y z : S
⊢ z • (single x 1 + single y 1 - single (x + y) 1) ∈ kerTotal R S
-- Mathlib/Computability/Tape.lean
theorem Tape.move_left_mk' {Γ} [Inhabited Γ] (L R : ListBlank Γ) :
    (Tape.mk' L R).move Dir.left = Tape.mk' L.tail (R.cons L.head)

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
L R : ListBlank Γ
⊢ move Dir.left (mk' L R) = mk' L.tail (ListBlank.cons L.head R)

Tactic:
simp only [Tape.move, Tape.mk', ListBlank.head_cons, eq_self_iff_true, ListBlank.cons_head_tail,
  and_self_iff, ListBlank.tail_cons]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
theorem betaIntegral_eval_one_right {u : ℂ} (hu : 0 < re u) : betaIntegral u 1 = 1 / u

Proof state:
u : ℂ
hu : 0 < u.re
⊢ u - 1 + 1 ≠ 0

Tactic:
rw [sub_add_cancel]

Result:
u : ℂ
hu : 0 < u.re
⊢ u ≠ 0

Proof state:
u : ℂ
hu : 0 < u.re
⊢ u ≠ 0

Tactic:
contrapose! hu

Result:
u : ℂ
hu : u = 0
⊢ u.re ≤ 0

Proof state:
u : ℂ
hu : 0 < u.re
⊢ u.betaIntegral 1 = 1 / u

Tactic:
simp_rw [betaIntegral, sub_self, cpow_zero, mul_one]

Result:
u : ℂ
hu : 0 < u.re
⊢ ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) = 1 / u

Proof state:
u : ℂ
hu : 0 < u.re
⊢ -1 < (u - 1).re

Tactic:
rwa [sub_re, one_re, ← sub_pos, sub_neg_eq_add, sub_add_cancel]

Result:
no goals

Proof state:
u : ℂ
hu : 0 < u.re
⊢ (↑1 ^ (u - 1 + 1) - ↑0 ^ (u - 1 + 1)) / (u - 1 + 1) = 1 / u

Tactic:
rw [ofReal_zero, ofReal_one, one_cpow, zero_cpow, sub_zero, sub_add_cancel]

Result:
u : ℂ
hu : 0 < u.re
⊢ u - 1 + 1 ≠ 0

Proof state:
u : ℂ
hu : u = 0
⊢ u.re ≤ 0

Tactic:
rw [hu, zero_re]

Result:
no goals

Proof state:
u : ℂ
hu : 0 < u.re
⊢ ∫ (x : ℝ) in 0 ..1, ↑x ^ (u - 1) = 1 / u

Tactic:
rw [integral_cpow (Or.inl _)]

Result:
u : ℂ
hu : 0 < u.re
⊢ (↑1 ^ (u - 1 + 1) - ↑0 ^ (u - 1 + 1)) / (u - 1 + 1) = 1 / u

u : ℂ
hu : 0 < u.re
⊢ -1 < (u - 1).re
-- Mathlib/Data/Set/Card.lean
theorem ncard_le_one_iff_eq (hs : s.Finite

Proof state:
case inr.intro.inr.intro
α : Type u_1
x : α
hs : autoParam {x}.Finite _auto✝
⊢ ∀ {a b : α}, a = x → b = x → a = b

Tactic:
simp only [forall_eq_apply_imp_iff, imp_self, implies_true]

Result:
no goals

Proof state:
case inr.intro
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
x : α
hx : x ∈ s
⊢ (s = ∅ ∨ ∃ a, s = {a}) → ∀ {a b : α}, a ∈ s → b ∈ s → a = b

Tactic:
rintro (rfl | ⟨a, rfl⟩)

Result:
case inr.intro.inl
α : Type u_1
x : α
hs : autoParam ∅.Finite _auto✝
hx : x ∈ ∅
⊢ ∀ {a b : α}, a ∈ ∅ → b ∈ ∅ → a = b

case inr.intro.inr.intro
α : Type u_1
x a : α
hs : autoParam {a}.Finite _auto✝
hx : x ∈ {a}
⊢ ∀ {a_1 b : α}, a_1 ∈ {a} → b ∈ {a} → a_1 = b

Proof state:
α : Type u_1
hs : autoParam ∅.Finite _auto✝
⊢ ∅.ncard ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
case inr.intro.inl
α : Type u_1
x : α
hs : autoParam ∅.Finite _auto✝
hx : x ∈ ∅
⊢ ∀ {a b : α}, a ∈ ∅ → b ∈ ∅ → a = b

Tactic:
exact (not_mem_empty _ hx).elim

Result:
no goals

Proof state:
case inr.intro
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
x : α
hx : x ∈ s
⊢ s.ncard ≤ 1 ↔ s = ∅ ∨ ∃ a, s = {a}

Tactic:
rw [ncard_le_one_iff hs]

Result:
case inr.intro
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
x : α
hx : x ∈ s
⊢ (∀ {a b : α}, a ∈ s → b ∈ s → a = b) ↔ s = ∅ ∨ ∃ a, s = {a}

Proof state:
case inr.intro.inr.intro
α : Type u_1
x a : α
hs : autoParam {a}.Finite _auto✝
hx : x ∈ {a}
⊢ ∀ {a_1 b : α}, a_1 ∈ {a} → b ∈ {a} → a_1 = b

Tactic:
simp_rw [mem_singleton_iff] at hx ⊢

Result:
case inr.intro.inr.intro
α : Type u_1
x a : α
hs : autoParam {a}.Finite _auto✝
hx : x = a
⊢ ∀ {a_1 b : α}, a_1 = a → b = a → a_1 = b

Proof state:
case inl
α : Type u_1
hs : autoParam ∅.Finite _auto✝
⊢ ∅.ncard ≤ 1 ↔ ∅ = ∅ ∨ ∃ a, ∅ = {a}

Tactic:
exact iff_of_true (by simp) (Or.inl rfl)

Result:
no goals

Proof state:
case inr.intro.inr.intro
α : Type u_1
x a : α
hs : autoParam {a}.Finite _auto✝
hx : x = a
⊢ ∀ {a_1 b : α}, a_1 = a → b = a → a_1 = b

Tactic:
subst hx

Result:
case inr.intro.inr.intro
α : Type u_1
x : α
hs : autoParam {x}.Finite _auto✝
⊢ ∀ {a b : α}, a = x → b = x → a = b

Proof state:
case inr.intro
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
x : α
hx : x ∈ s
⊢ (∀ {a b : α}, a ∈ s → b ∈ s → a = b) ↔ s = ∅ ∨ ∃ a, s = {a}

Tactic:
refine ⟨fun h ↦ Or.inr ⟨x, (singleton_subset_iff.mpr hx).antisymm' fun y hy ↦ h hy hx⟩, ?_⟩

Result:
case inr.intro
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
x : α
hx : x ∈ s
⊢ (s = ∅ ∨ ∃ a, s = {a}) → ∀ {a b : α}, a ∈ s → b ∈ s → a = b

Proof state:
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
⊢ s.ncard ≤ 1 ↔ s = ∅ ∨ ∃ a, s = {a}

Tactic:
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty

Result:
case inl
α : Type u_1
hs : autoParam ∅.Finite _auto✝
⊢ ∅.ncard ≤ 1 ↔ ∅ = ∅ ∨ ∃ a, ∅ = {a}

case inr.intro
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
x : α
hx : x ∈ s
⊢ s.ncard ≤ 1 ↔ s = ∅ ∨ ∃ a, s = {a}
-- Mathlib/Analysis/Normed/Ring/SeminormFromConst.lean
theorem seminormFromConst_le_seminorm (x : R) : seminormFromConst' hf1 hc hpm x ≤ f x

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
n : ℕ
hn : 1 ≤ n
⊢ 0 < f c ^ n

Tactic:
positivity

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ ∀ (b : ℕ), 1 ≤ b → seminormFromConst_seq c f x b ≤ f x

Tactic:
intro n hn

Result:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
n : ℕ
hn : 1 ≤ n
⊢ seminormFromConst_seq c f x n ≤ f x

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ seminormFromConst' hf1 hc hpm x ≤ f x

Tactic:
apply le_of_tendsto (seminormFromConst_isLimit hf1 hc hpm x)

Result:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ ∀ᶠ (c_1 : ℕ) in atTop, seminormFromConst_seq c f x c_1 ≤ f x

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ ∀ᶠ (c_1 : ℕ) in atTop, seminormFromConst_seq c f x c_1 ≤ f x

Tactic:
simp only [eventually_atTop, ge_iff_le]

Result:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → seminormFromConst_seq c f x b ≤ f x

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → seminormFromConst_seq c f x b ≤ f x

Tactic:
use 1

Result:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ ∀ (b : ℕ), 1 ≤ b → seminormFromConst_seq c f x b ≤ f x

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
n : ℕ
hn : 1 ≤ n
⊢ f (x * c ^ n) ≤ f x * f (c ^ n)

Tactic:
exact map_mul_le_mul ..

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
n : ℕ
hn : 1 ≤ n
⊢ seminormFromConst_seq c f x n ≤ f x

Tactic:
rw [seminormFromConst_seq, div_le_iff₀ (by positivity), ← hpm c hn]

Result:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
n : ℕ
hn : 1 ≤ n
⊢ f (x * c ^ n) ≤ f x * f (c ^ n)
-- Mathlib/Data/ENNReal/Inv.lean
theorem div_le_of_le_mul (h : a ≤ b * c) : a / c ≤ b

Proof state:
case pos
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : c = 0
⊢ a / c ≤ b

Tactic:
have : a = 0 := by simpa [h0] using h

Result:
case pos
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : c = 0
this : a = 0
⊢ a / c ≤ b

Proof state:
case pos
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : c = 0
this : a = 0
⊢ a / c ≤ b

Tactic:
simp [*]

Result:
no goals

Proof state:
case pos
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : ¬c = 0
hinf : c = ⊤
⊢ a / c ≤ b

Tactic:
simp [hinf]

Result:
no goals

Proof state:
case neg
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : ¬c = 0
hinf : ¬c = ⊤
⊢ a / c ≤ b

Tactic:
exact (ENNReal.div_le_iff_le_mul (Or.inl h0) (Or.inl hinf)).2 h

Result:
no goals

Proof state:
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : c = 0
⊢ a = 0

Tactic:
simpa [h0] using h

Result:
no goals

Proof state:
case neg
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : ¬c = 0
⊢ a / c ≤ b

Tactic:
by_cases hinf : c = ∞

Result:
case pos
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : ¬c = 0
hinf : c = ⊤
⊢ a / c ≤ b

case neg
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : ¬c = 0
hinf : ¬c = ⊤
⊢ a / c ≤ b

Proof state:
a b c : ℝ≥0∞
h : a ≤ b * c
⊢ a / c ≤ b

Tactic:
by_cases h0 : c = 0

Result:
case pos
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : c = 0
⊢ a / c ≤ b

case neg
a b c : ℝ≥0∞
h : a ≤ b * c
h0 : ¬c = 0
⊢ a / c ≤ b
-- Mathlib/Data/Multiset/AddSub.lean
protected lemma sub_add_cancel (hts : t ≤ s) : s - t + t = s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
hts : t ≤ s
⊢ s - t + t = s

Tactic:
ext a

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
hts : t ≤ s
a : α
⊢ count a (s - t + t) = count a s

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
hts : t ≤ s
a : α
⊢ count a (s - t + t) = count a s

Tactic:
simp [Nat.sub_add_cancel <| count_le_of_le _ hts]

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
theorem mul_pos {a b : ℝ} : 0 < a → 0 < b → 0 < a * b

Proof state:
case h
b : ℝ
a : CauSeq ℚ abs
⊢ 0 < mk a → 0 < b → 0 < mk a * b

Tactic:
induction' b using Real.ind_mk with b

Result:
case h.h
a b : CauSeq ℚ abs
⊢ 0 < mk a → 0 < mk b → 0 < mk a * mk b

Proof state:
a b : ℝ
⊢ 0 < a → 0 < b → 0 < a * b

Tactic:
induction' a using Real.ind_mk with a

Result:
case h
b : ℝ
a : CauSeq ℚ abs
⊢ 0 < mk a → 0 < b → 0 < mk a * b

Proof state:
case h.h
a b : CauSeq ℚ abs
⊢ 0 < mk a → 0 < mk b → 0 < mk a * mk b

Tactic:
simpa only [mk_lt, mk_pos, ← mk_mul] using CauSeq.mul_pos

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem transpose_col (v : m → α) : (Matrix.col ι v)ᵀ = Matrix.row ι v

Proof state:
m : Type u_2
α : Type v
ι : Type u_6
v : m → α
⊢ (col ι v)ᵀ = row ι v

Tactic:
ext

Result:
case a
m : Type u_2
α : Type v
ι : Type u_6
v : m → α
i✝ : ι
j✝ : m
⊢ (col ι v)ᵀ i✝ j✝ = row ι v i✝ j✝

Proof state:
case a
m : Type u_2
α : Type v
ι : Type u_6
v : m → α
i✝ : ι
j✝ : m
⊢ (col ι v)ᵀ i✝ j✝ = row ι v i✝ j✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Lie/BaseChange.lean
@[simp]
lemma LieModule.toEnd_baseChange (x : L) :
    toEnd A (A ⊗[R] L) (A ⊗[R] M) (1 ⊗ₜ x) = (toEnd R L M x).baseChange A

Proof state:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : L
⊢ (toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x) = LinearMap.baseChange A ((toEnd R L M) x)

Tactic:
ext

Result:
case a.h.h
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : L
x✝ : M
⊢ ((TensorProduct.AlgebraTensorModule.curry ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x))) 1) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (LinearMap.baseChange A ((toEnd R L M) x))) 1) x✝

Proof state:
case a.h.h
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : L
x✝ : M
⊢ ((TensorProduct.AlgebraTensorModule.curry ((toEnd A (A ⊗[R] L) (A ⊗[R] M)) (1 ⊗ₜ[R] x))) 1) x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (LinearMap.baseChange A ((toEnd R L M) x))) 1) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem contDiff_pi : ContDiff 𝕜 n Φ ↔ ∀ i, ContDiff 𝕜 n fun x => Φ x i

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
n : WithTop ℕ∞
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
⊢ ContDiff 𝕜 n Φ ↔ ∀ (i : ι), ContDiff 𝕜 n fun x => Φ x i

Tactic:
simp only [← contDiffOn_univ, contDiffOn_pi]

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
@[simp]
lemma linearDeriv_apply [DecidableEq ι] [Fintype ι] (f : MultilinearMap R M₁ M₂)
    (x y : (i : ι) → M₁ i) :
    f.linearDeriv x y = ∑ i, f (update x i (y i))

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : MultilinearMap R M₁ M₂
x y : (i : ι) → M₁ i
⊢ (f.linearDeriv x) y = ∑ i : ι, f (update x i (y i))

Tactic:
unfold linearDeriv

Result:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : MultilinearMap R M₁ M₂
x y : (i : ι) → M₁ i
⊢ (∑ i : ι, f.toLinearMap x i ∘ₗ LinearMap.proj i) y = ∑ i : ι, f (update x i (y i))

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : MultilinearMap R M₁ M₂
x y : (i : ι) → M₁ i
⊢ (∑ i : ι, f.toLinearMap x i ∘ₗ LinearMap.proj i) y = ∑ i : ι, f (update x i (y i))

Tactic:
simp only [LinearMap.coeFn_sum, LinearMap.coe_comp, LinearMap.coe_proj, Finset.sum_apply,
  Function.comp_apply, Function.eval, toLinearMap_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mkVector_beq_mkVector [BEq α] {a b : α} {n : Nat} :
    (mkVector n a == mkVector n b) = (n == 0 || a == b)

Proof state:
case succ
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
⊢ ((n == 0 || a == b) && a == b) = (n + 1 == 0 || a == b)

Tactic:
rw [Bool.eq_iff_iff]

Result:
case succ
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
⊢ ((n == 0 || a == b) && a == b) = true ↔ (n + 1 == 0 || a == b) = true

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
⊢ (mkVector n a == mkVector n b) = (n == 0 || a == b)

Tactic:
cases n with
| zero => simp
| succ n =>
  rw [mkVector_succ, mkVector_succ, push_beq_push, mkVector_beq_mkVector]
  rw [Bool.eq_iff_iff]
  simp +contextual

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
⊢ ((n == 0 || a == b) && a == b) = true ↔ (n + 1 == 0 || a == b) = true

Tactic:
simp +contextual

Result:
no goals

Proof state:
case zero
α : Type u_1
inst✝ : BEq α
a b : α
⊢ (mkVector 0 a == mkVector 0 b) = (0 == 0 || a == b)

Tactic:
simp

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
⊢ (mkVector (n + 1) a == mkVector (n + 1) b) = (n + 1 == 0 || a == b)

Tactic:
rw [mkVector_succ, mkVector_succ, push_beq_push, mkVector_beq_mkVector]

Result:
case succ
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
⊢ ((n == 0 || a == b) && a == b) = (n + 1 == 0 || a == b)
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasStrictDerivAt.smul (hc : HasStrictDerivAt c c' x) (hf : HasStrictDerivAt f f' x) :
    HasStrictDerivAt (fun y => c y • f y) (c x • f' + c' • f x) x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasStrictDerivAt c c' x
hf : HasStrictDerivAt f f' x
⊢ HasStrictDerivAt (fun y => c y • f y) (c x • f' + c' • f x) x

Tactic:
simpa using (hc.smul hf).hasStrictDerivAt

Result:
no goals
-- Mathlib/Algebra/Module/SpanRank.lean
/-- A submodule is finitely generated if and only if its `spanRank` is equal to its `spanFinrank`.
-/
lemma fg_iff_spanRank_eq_spanFinrank {p : Submodule R M} : p.spanRank = p.spanFinrank ↔ p.FG

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ ↑(toNat p.spanRank) = p.spanRank ↔ p.spanRank < ℵ₀

Tactic:
exact cast_toNat_eq_iff_lt_aleph0

Result:
no goals

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ p.spanRank = ↑p.spanFinrank ↔ p.FG

Tactic:
rw [spanFinrank, ← spanRank_finite_iff_fg, eq_comm]

Result:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ ↑(toNat p.spanRank) = p.spanRank ↔ p.spanRank < ℵ₀
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem find?_mkArray_eq_none_iff {n : Nat} {a : α} {p : α → Bool} :
    (mkArray n a).find? p = none ↔ n = 0 ∨ !p a

Proof state:
α : Type u_1
n : Nat
a : α
p : α → Bool
⊢ find? p (mkArray n a) = none ↔ n = 0 ∨ (!p a) = true

Tactic:
simp [← List.toArray_replicate, List.find?_replicate_eq_none_iff, Classical.or_iff_not_imp_left]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sinh_sub : sinh (x - y) = sinh x * cosh y - cosh x * sinh y

Proof state:
x y : ℂ
⊢ sinh (x - y) = sinh x * cosh y - cosh x * sinh y

Tactic:
simp [sub_eq_add_neg, sinh_add, sinh_neg, cosh_neg]

Result:
no goals
-- Mathlib/FieldTheory/Galois/Profinite.lean
@[simp]
lemma map_comp {L₁ L₂ L₃ : (FiniteGaloisIntermediateField k K)ᵒᵖ} (f : L₁ ⟶ L₂) (g : L₂ ⟶ L₃) :
    finGaloisGroupMap (f ≫ g) = finGaloisGroupMap f ≫ finGaloisGroupMap g

Proof state:
case h.h.h.mk.mk.mk.h
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L₁ : IntermediateField k K
finiteDimensional✝² : FiniteDimensional k ↥L₁
isGalois✝² : IsGalois k ↥L₁
L₂ : IntermediateField k K
finiteDimensional✝¹ : FiniteDimensional k ↥L₂
isGalois✝¹ : IsGalois k ↥L₂
f : op (FiniteGaloisIntermediateField.mk L₁) ⟶ op (FiniteGaloisIntermediateField.mk L₂)
L₃ : IntermediateField k K
finiteDimensional✝ : FiniteDimensional k ↥L₃
isGalois✝ : IsGalois k ↥L₃
g : op (FiniteGaloisIntermediateField.mk L₂) ⟶ op (FiniteGaloisIntermediateField.mk L₃)
algInst✝² : Algebra ↥(unop (op (FiniteGaloisIntermediateField.mk L₃))).toSubsemiring
  ↥(unop (op (FiniteGaloisIntermediateField.mk L₂))).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst✝¹ : Algebra ↥(unop (op (FiniteGaloisIntermediateField.mk L₂))).toSubsemiring
  ↥(unop (op (FiniteGaloisIntermediateField.mk L₁))).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
algInst✝ : Algebra ↥(unop (op (FiniteGaloisIntermediateField.mk L₃))).toSubsemiring
  ↥(unop (op (FiniteGaloisIntermediateField.mk L₁))).toSubsemiring :=
  (Subsemiring.inclusion ⋯).toAlgebra
this✝² : IsScalarTower k ↥L₂ ↥L₁
this✝¹ : IsScalarTower k ↥L₃ ↥L₁
this✝ : IsScalarTower k ↥L₃ ↥L₂
this : IsScalarTower ↥L₃ ↥L₂ ↥L₁
⊢ ConcreteCategory.hom (finGaloisGroupMap (f ≫ g)) = ConcreteCategory.hom (finGaloisGroupMap f ≫ finGaloisGroupMap g)

Tactic:
apply IsScalarTower.AlgEquiv.restrictNormalHom_comp k L₃ L₂ L₁

Result:
no goals
-- Mathlib/Data/Int/ModEq.lean
theorem modEq_neg : a ≡ b [ZMOD -n] ↔ a ≡ b [ZMOD n]

Proof state:
n a b : ℤ
⊢ a ≡ b [ZMOD -n] ↔ a ≡ b [ZMOD n]

Tactic:
simp [modEq_iff_dvd]

Result:
no goals