harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/PurelyInseparable/Tower.lean
theorem lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic [Algebra.IsAlgebraic F E] :
    Cardinal.lift.{w} (sepDegree F E) * Cardinal.lift.{v} (sepDegree E K) =
    Cardinal.lift.{v} (sepDegree F K)

Proof state:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsAlgebraic F E
h :
  Cardinal.lift.{w, v} (Module.rank F ↥(separableClosure F E)) *
      Cardinal.lift.{v, w} (sepDegree (↥(separableClosure F E)) K) =
    Cardinal.lift.{v, w} (sepDegree F K)
this : IsPurelyInseparable (↥(separableClosure F E)) E
⊢ Cardinal.lift.{w, v} (sepDegree F E) * Cardinal.lift.{v, w} (sepDegree E K) = Cardinal.lift.{v, w} (sepDegree F K)

Tactic:
rwa [sepDegree_eq_of_isPurelyInseparable (separableClosure F E) E K] at h

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsAlgebraic F E
⊢ Cardinal.lift.{w, v} (sepDegree F E) * Cardinal.lift.{v, w} (sepDegree E K) = Cardinal.lift.{v, w} (sepDegree F K)

Tactic:
have h := lift_rank_mul_lift_sepDegree_of_isSeparable F (separableClosure F E) K

Result:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsAlgebraic F E
h :
  Cardinal.lift.{w, v} (Module.rank F ↥(separableClosure F E)) *
      Cardinal.lift.{v, w} (sepDegree (↥(separableClosure F E)) K) =
    Cardinal.lift.{v, w} (sepDegree F K)
⊢ Cardinal.lift.{w, v} (sepDegree F E) * Cardinal.lift.{v, w} (sepDegree E K) = Cardinal.lift.{v, w} (sepDegree F K)

Proof state:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsAlgebraic F E
h :
  Cardinal.lift.{w, v} (Module.rank F ↥(separableClosure F E)) *
      Cardinal.lift.{v, w} (sepDegree (↥(separableClosure F E)) K) =
    Cardinal.lift.{v, w} (sepDegree F K)
⊢ Cardinal.lift.{w, v} (sepDegree F E) * Cardinal.lift.{v, w} (sepDegree E K) = Cardinal.lift.{v, w} (sepDegree F K)

Tactic:
haveI := separableClosure.isPurelyInseparable F E

Result:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsAlgebraic F E
h :
  Cardinal.lift.{w, v} (Module.rank F ↥(separableClosure F E)) *
      Cardinal.lift.{v, w} (sepDegree (↥(separableClosure F E)) K) =
    Cardinal.lift.{v, w} (sepDegree F K)
this : IsPurelyInseparable (↥(separableClosure F E)) E
⊢ Cardinal.lift.{w, v} (sepDegree F E) * Cardinal.lift.{v, w} (sepDegree E K) = Cardinal.lift.{v, w} (sepDegree F K)
-- Mathlib/Data/Finset/Sym.lean
theorem not_isDiag_mk_of_mem_offDiag {a : α × α} (h : a ∈ s.offDiag) :
    ¬ (Sym2.mk a).IsDiag

Proof state:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α × α
h : a ∈ s.offDiag
⊢ ¬(Sym2.mk a).IsDiag

Tactic:
rw [Sym2.isDiag_iff_proj_eq]

Result:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α × α
h : a ∈ s.offDiag
⊢ ¬a.1 = a.2

Proof state:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α × α
h : a ∈ s.offDiag
⊢ ¬a.1 = a.2

Tactic:
exact (mem_offDiag.1 h).2.2

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem weightedOrder_monomial_of_ne_zero {d : σ →₀ ℕ} {a : R} (h : a ≠ 0) :
    weightedOrder w (monomial R d a) = weight w d

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
h : a ≠ 0
⊢ weightedOrder w ((monomial R d) a) = ↑((weight w) d)

Tactic:
classical
rw [weightedOrder_monomial, if_neg h]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
h : a ≠ 0
⊢ weightedOrder w ((monomial R d) a) = ↑((weight w) d)

Tactic:
rw [weightedOrder_monomial, if_neg h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem mem_attachWith (l : Vector α n) {q : α → Prop} (H) (x : {x // q x}) :
    x ∈ l.attachWith q H ↔ x.1 ∈ l

Proof state:
case mk
α : Type u_1
q : α → Prop
x : { x // q x }
l : Array α
H : ∀ (x : α), x ∈ { toArray := l, size_toArray := ⋯ } → q x
⊢ x ∈ { toArray := l, size_toArray := ⋯ }.attachWith q H ↔ x.val ∈ { toArray := l, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : Vector α n
q : α → Prop
H : ∀ (x : α), x ∈ l → q x
x : { x // q x }
⊢ x ∈ l.attachWith q H ↔ x.val ∈ l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
q : α → Prop
x : { x // q x }
l : Array α
H : ∀ (x : α), x ∈ { toArray := l, size_toArray := ⋯ } → q x
⊢ x ∈ { toArray := l, size_toArray := ⋯ }.attachWith q H ↔ x.val ∈ { toArray := l, size_toArray := ⋯ }
-- Mathlib/Order/Filter/IndicatorFunction.lean
theorem Filter.EventuallyEq.mulIndicator_one [One β] {l : Filter α} {f : α → β} {s : Set α}
    (hf : f =ᶠ[l] 1) : s.mulIndicator f =ᶠ[l] 1 :=
  hf.mulIndicator.trans <| by rw [mulIndicator_one']

Proof state:
α : Type u_1
β : Type u_2
inst✝ : One β
l : Filter α
f : α → β
s : Set α
hf : f =ᶠ[l] 1
⊢ s.mulIndicator 1 =ᶠ[l] 1

Tactic:
rw [mulIndicator_one']

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZeta.lean
lemma differentiableAt_expZeta (a : UnitAddCircle) (s : ℂ) (hs : s ≠ 1 ∨ a ≠ 0) :
    DifferentiableAt ℂ (expZeta a) s

Proof state:
case hf
a : UnitAddCircle
s : ℂ
hs : s ≠ 1 ∨ a ≠ 0
⊢ DifferentiableAt ℂ (cosZeta a) s

Tactic:
exact differentiableAt_cosZeta a hs

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
hs : s ≠ 1 ∨ a ≠ 0
⊢ DifferentiableAt ℂ (expZeta a) s

Tactic:
apply DifferentiableAt.add

Result:
case hf
a : UnitAddCircle
s : ℂ
hs : s ≠ 1 ∨ a ≠ 0
⊢ DifferentiableAt ℂ (cosZeta a) s

case hg
a : UnitAddCircle
s : ℂ
hs : s ≠ 1 ∨ a ≠ 0
⊢ DifferentiableAt ℂ (fun y => I * sinZeta a y) s

Proof state:
case hg
a : UnitAddCircle
s : ℂ
hs : s ≠ 1 ∨ a ≠ 0
⊢ DifferentiableAt ℂ (fun y => I * sinZeta a y) s

Tactic:
apply (differentiableAt_const _).mul (differentiableAt_sinZeta a s)

Result:
no goals
-- Mathlib/ModelTheory/DirectLimit.lean
theorem exists_of (z : DirectLimit G f) : ∃ i x, of L ι G f i x = z :=
  ⟨z.out.1, z.out.2, by simp⟩

Proof state:
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)
inst✝ : Nonempty ι
z : DirectLimit G f
⊢ (of L ι G f (Quotient.out z).fst) (Quotient.out z).snd = z

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem sdiff_sup_cancel (h : b ≤ a) : a \ b ⊔ b = a

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
h : b ≤ a
⊢ a \ b ⊔ b = a

Tactic:
rw [sup_comm, sup_sdiff_cancel_right h]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
@[simp]
lemma leRec_self {n} {motive : (m : ℕ) → n ≤ m → Sort*}
    (refl : motive n (Nat.le_refl _))
    (le_succ_of_le : ∀ ⦃k⦄ (h : n ≤ k), motive k h → motive (k + 1) (le_succ_of_le h)) :
    (leRec (motive := motive) refl le_succ_of_le (Nat.le_refl _) :
    motive n (Nat.le_refl _)) = refl

Proof state:
n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
⊢ leRec refl le_succ_of_le ⋯ = refl

Tactic:
cases n <;> simp [leRec, Or.by_cases, dif_neg]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem eventually_const {f : Filter α} [t : NeBot f] {p : Prop} : (∀ᶠ _ in f, p) ↔ p

Proof state:
α : Type u
f : Filter α
t : f.NeBot
p : Prop
⊢ (∀ᶠ (x : α) in f, p) ↔ p

Tactic:
by_cases h : p <;> simp [h, t.ne]

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean
theorem isZeroAtImInfty_iff {α : Type*} [SeminormedAddGroup α] {f : ℍ → α} :
    IsZeroAtImInfty f ↔ ∀ ε : ℝ, 0 < ε → ∃ A : ℝ, ∀ z : ℍ, A ≤ im z → ‖f z‖ ≤ ε :=
  (atImInfty_basis.tendsto_iff Metric.nhds_basis_closedBall).trans <| by simp

Proof state:
α : Type u_1
inst✝ : SeminormedAddGroup α
f : ℍ → α
⊢ (∀ (ib : ℝ), 0 < ib → ∃ ia, True ∧ ∀ x ∈ im ⁻¹' Set.Ici ia, f x ∈ Metric.closedBall 0 ib) ↔
    ∀ (ε : ℝ), 0 < ε → ∃ A, ∀ (z : ℍ), A ≤ z.im → ‖f z‖ ≤ ε

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/MeanInequalitiesPow.lean
theorem rpow_add_rpow_le_add {p : ℝ} (a b : ℝ≥0∞) (hp1 : 1 ≤ p) :
    (a ^ p + b ^ p) ^ (1 / p) ≤ a + b

Proof state:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p⁻¹⁻¹

Tactic:
rw [inv_inv]

Result:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Proof state:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ (a ^ p + b ^ p) ^ (1 / p) ≤ a + b

Tactic:
rw [one_div, ← @ENNReal.le_rpow_inv_iff _ _ p⁻¹ (by simp [lt_of_lt_of_le zero_lt_one hp1])]

Result:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p⁻¹⁻¹

Proof state:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
exact add_rpow_le_rpow_add _ _ hp1

Result:
no goals

Proof state:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ 0 < p⁻¹

Tactic:
simp [lt_of_lt_of_le zero_lt_one hp1]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_sdiff_left : a ∆ b \ a = b \ a

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ a ∆ b \ a = b \ a

Tactic:
rw [symmDiff_def, sup_sdiff, sdiff_idem, sdiff_sdiff_self, bot_sup_eq]

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
/-- Specialization of `Finset.card_nbij'` that automatically fills in most arguments.

See `Fintype.card_equiv` for the version where `s` and `t` are `univ`. -/
lemma card_equiv (e : α ≃ β) (hst : ∀ i, i ∈ s ↔ e i ∈ t) : #s = #t

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α ≃ β
hst : ∀ (i : α), i ∈ s ↔ e i ∈ t
⊢ #s = #t

Tactic:
refine card_nbij' e e.symm ?_ ?_ ?_ ?_ <;> simp [hst]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filter_congr {as bs : Array α} (h : as = bs)
    {f : α → Bool} {g : α → Bool} (h' : f = g) {start stop start' stop' : Nat}
    (h₁ : start = start') (h₂ : stop = stop') :
    filter f as start stop = filter g bs start' stop'

Proof state:
α : Type u_1
as bs : Array α
h : as = bs
f g : α → Bool
h' : f = g
start stop start' stop' : Nat
h₁ : start = start'
h₂ : stop = stop'
⊢ filter f as start stop = filter g bs start' stop'

Tactic:
congr

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem eq_false_imp_eq_true : ∀ {b : Bool}, (b = false → b = true) ↔ (b = true)

Proof state:
⊢ ∀ {b : Bool}, b = false → b = true ↔ b = true

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/AC.lean
theorem Context.sort_loop_nonEmpty (xs : List Nat) (h : xs ≠ []) : sort.loop xs ys ≠ []

Proof state:
case cons
y : Nat
tail✝ : List Nat
ih : ∀ (xs : List Nat), xs ≠ [] → sort.loop xs tail✝ ≠ []
xs : List Nat
h : xs ≠ []
⊢ sort.loop xs (y :: tail✝) ≠ []

Tactic:
simp [sort.loop]

Result:
case cons
y : Nat
tail✝ : List Nat
ih : ∀ (xs : List Nat), xs ≠ [] → sort.loop xs tail✝ ≠ []
xs : List Nat
h : xs ≠ []
⊢ ¬sort.loop (insert y xs) tail✝ = []

Proof state:
case cons.h
y : Nat
tail✝ : List Nat
ih : ∀ (xs : List Nat), xs ≠ [] → sort.loop xs tail✝ ≠ []
xs : List Nat
h : xs ≠ []
⊢ insert y xs ≠ []

Tactic:
apply insert_nonEmpty

Result:
no goals

Proof state:
ys xs : List Nat
h : xs ≠ []
⊢ sort.loop xs ys ≠ []

Tactic:
induction ys generalizing xs with
| nil => simp [sort.loop]; assumption
| cons y _  ih => simp [sort.loop]; apply ih; apply insert_nonEmpty

Result:
no goals

Proof state:
case cons
y : Nat
tail✝ : List Nat
ih : ∀ (xs : List Nat), xs ≠ [] → sort.loop xs tail✝ ≠ []
xs : List Nat
h : xs ≠ []
⊢ ¬sort.loop (insert y xs) tail✝ = []

Tactic:
apply ih

Result:
case cons.h
y : Nat
tail✝ : List Nat
ih : ∀ (xs : List Nat), xs ≠ [] → sort.loop xs tail✝ ≠ []
xs : List Nat
h : xs ≠ []
⊢ insert y xs ≠ []

Proof state:
case nil
xs : List Nat
h : xs ≠ []
⊢ sort.loop xs [] ≠ []

Tactic:
simp [sort.loop]

Result:
case nil
xs : List Nat
h : xs ≠ []
⊢ ¬xs = []

Proof state:
case nil
xs : List Nat
h : xs ≠ []
⊢ ¬xs = []

Tactic:
assumption

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Subcategory.lean
lemma W_iff {X Y : C} (f : X ⟶ Y) :
    S.W f ↔ ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ X⟦(1 : ℤ)⟧)
      (_ : Triangle.mk f g h ∈ distTriang C), S.P Z

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
S : Subcategory C
X Y : C
f : X ⟶ Y
⊢ S.W f ↔ ∃ Z g h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), S.P Z

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasFDerivAt.comp_hasDerivWithinAt_of_eq (hl : HasFDerivAt l l' y)
    (hf : HasDerivWithinAt f f' s x) (hy : y = f x) :
    HasDerivWithinAt (l ∘ f) (l' f') s x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
hl : HasFDerivAt l l' (f x)
hf : HasDerivWithinAt f f' s x
hy : y = f x
⊢ HasDerivWithinAt (l ∘ f) (l' f') s x

Tactic:
exact hl.comp_hasDerivWithinAt x hf

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
hl : HasFDerivAt l l' y
hf : HasDerivWithinAt f f' s x
hy : y = f x
⊢ HasDerivWithinAt (l ∘ f) (l' f') s x

Tactic:
rw [hy] at hl

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
hl : HasFDerivAt l l' (f x)
hf : HasDerivWithinAt f f' s x
hy : y = f x
⊢ HasDerivWithinAt (l ∘ f) (l' f') s x
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem lift_uniq (H : Set.range g.base ⊆ Set.range f.base) (l : Y ⟶ X) (hl : l ≫ f = g) :
    l = lift f g H

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
H : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
l : Y ⟶ X
hl : l ≫ f = g
⊢ l = lift f g H

Tactic:
rw [← cancel_mono f, hl, lift_fac]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extChartAt_prod (x : M × M') :
    extChartAt (I.prod I') x = (extChartAt I x.1).prod (extChartAt I' x.2)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
inst✝¹ : ChartedSpace H M
inst✝ : ChartedSpace H' M'
x : M × M'
⊢ extChartAt (I.prod I') x = (extChartAt I x.1).prod (extChartAt I' x.2)

Tactic:
simp only [mfld_simps]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
inst✝¹ : ChartedSpace H M
inst✝ : ChartedSpace H' M'
x : M × M'
⊢ (chartAt H x.1).prod (chartAt H' x.2).toPartialEquiv ≫ I.prod I'.toPartialEquiv =
    ((chartAt H x.1).toPartialEquiv ≫ I.toPartialEquiv).prod ((chartAt H' x.2).toPartialEquiv ≫ I'.toPartialEquiv)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : TopologicalSpace H
inst✝⁶ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
inst✝¹ : ChartedSpace H M
inst✝ : ChartedSpace H' M'
x : M × M'
⊢ (chartAt H x.1).prod (chartAt H' x.2).toPartialEquiv ≫ I.prod I'.toPartialEquiv =
    ((chartAt H x.1).toPartialEquiv ≫ I.toPartialEquiv).prod ((chartAt H' x.2).toPartialEquiv ≫ I'.toPartialEquiv)

Tactic:
rw [PartialEquiv.prod_trans]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem neg_closedBall (p : Seminorm 𝕜 E) (r : ℝ) (x : E) :
    -closedBall p x r = closedBall p (-x) r

Proof state:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x x✝ : E
⊢ x✝ ∈ -p.closedBall x r ↔ x✝ ∈ p.closedBall (-x) r

Tactic:
rw [Set.mem_neg, mem_closedBall, mem_closedBall, ← neg_add', sub_neg_eq_add, map_neg_eq_map]

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x : E
⊢ -p.closedBall x r = p.closedBall (-x) r

Tactic:
ext

Result:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
x x✝ : E
⊢ x✝ ∈ -p.closedBall x r ↔ x✝ ∈ p.closedBall (-x) r
-- Mathlib/Combinatorics/SetFamily/Shatter.lean
lemma shatters_iff : 𝒜.Shatters s ↔ 𝒜.image (fun t ↦ s ∩ t) = s.powerset :=
  ⟨fun h ↦ by ext t; rw [mem_image, mem_powerset, h.subset_iff],
    fun h t ht ↦ by rwa [← mem_powerset, ← h, mem_image] at ht⟩

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : image (fun t => s ∩ t) 𝒜 = s.powerset
t : Finset α
ht : t ⊆ s
⊢ ∃ u ∈ 𝒜, s ∩ u = t

Tactic:
rwa [← mem_powerset, ← h, mem_image] at ht

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
⊢ image (fun t => s ∩ t) 𝒜 = s.powerset

Tactic:
ext t

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
t : Finset α
⊢ t ∈ image (fun t => s ∩ t) 𝒜 ↔ t ∈ s.powerset

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
t : Finset α
⊢ t ∈ image (fun t => s ∩ t) 𝒜 ↔ t ∈ s.powerset

Tactic:
rw [mem_image, mem_powerset, h.subset_iff]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Basic.lean
lemma SurjOn.perm_pow : SurjOn f s s → ∀ n : ℕ, SurjOn (f ^ n) s s

Proof state:
α : Type u_1
f : Perm α
s : Set α
⊢ SurjOn (⇑f) s s → ∀ (n : ℕ), SurjOn (⇑f)^[n] s s

Tactic:
exact SurjOn.iterate

Result:
no goals

Proof state:
α : Type u_1
f : Perm α
s : Set α
⊢ SurjOn (⇑f) s s → ∀ (n : ℕ), SurjOn (⇑(f ^ n)) s s

Tactic:
simp_rw [Equiv.Perm.coe_pow]

Result:
α : Type u_1
f : Perm α
s : Set α
⊢ SurjOn (⇑f) s s → ∀ (n : ℕ), SurjOn (⇑f)^[n] s s
-- Mathlib/Algebra/Order/Interval/Set/Monoid.lean
theorem image_const_add_Ioi : (fun x => a + x) '' Ioi b = Ioi (a + b)

Proof state:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b : M
⊢ (fun x => a + x) '' Ioi b = Ioi (a + b)

Tactic:
simp only [add_comm a, image_add_const_Ioi]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Completion.lean
@[simp]
lemma enorm_coe {E} [SeminormedAddCommGroup E] (x : E) : ‖(x : Completion E)‖ₑ = ‖x‖ₑ

Proof state:
E : Type u_2
inst✝ : SeminormedAddCommGroup E
x : E
⊢ ‖↑x‖ₑ = ‖x‖ₑ

Tactic:
simp [enorm]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Iio_add_one_eq_Iic_of_not_isMax (hb : ¬ IsMax b) : Iio (b + 1) = Iic b

Proof state:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
b : α
hb : ¬IsMax b
⊢ Iio (b + 1) = Iic b

Tactic:
simpa [succ_eq_add_one] using Iio_succ_eq_Iic_of_not_isMax hb

Result:
no goals
-- Mathlib/Data/Int/Order/Units.lean
theorem units_sq (u : ℤˣ) : u ^ 2 = 1

Proof state:
u : ℤˣ
⊢ u ^ 2 = 1

Tactic:
rw [Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one, isUnit_sq u.isUnit]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- `δ` is the function underlying the arithmetic function `1`. -/
lemma ArithmeticFunction.one_eq_delta : ↗(1 : ArithmeticFunction ℂ) = δ

Proof state:
case h
x✝ : ℕ
⊢ 1 x✝ = δ x✝

Tactic:
simp [one_apply, LSeries.delta]

Result:
no goals

Proof state:
⊢ (fun n => 1 n) = δ

Tactic:
ext

Result:
case h
x✝ : ℕ
⊢ 1 x✝ = δ x✝
-- Mathlib/RingTheory/Finiteness/Finsupp.lean
theorem _root_.Module.Finite.of_submodule_quotient (N : Submodule R M) [Module.Finite R N]
    [Module.Finite R (M ⧸ N)] : Module.Finite R M where
  fg_top := fg_of_fg_map_of_fg_inf_ker N.mkQ
    (by simpa only [map_top, range_mkQ] using Module.finite_def.mp ‹_›) <| by
    simpa only [top_inf_eq, ker_mkQ] using Module.Finite.iff_fg.mp ‹_›

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Submodule R M
inst✝¹ : Module.Finite R ↥N
inst✝ : Module.Finite R (M ⧸ N)
⊢ (⊤ ⊓ LinearMap.ker N.mkQ).FG

Tactic:
simpa only [top_inf_eq, ker_mkQ] using Module.Finite.iff_fg.mp ‹_›

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Submodule R M
inst✝¹ : Module.Finite R ↥N
inst✝ : Module.Finite R (M ⧸ N)
⊢ (map N.mkQ ⊤).FG

Tactic:
simpa only [map_top, range_mkQ] using Module.finite_def.mp ‹_›

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
lemma exists_set_linearIndependent_of_lt_rank {n : Cardinal} (hn : n < Module.rank R M) :
    ∃ s : Set M, #s = n ∧ LinearIndepOn R id s

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : Cardinal.{v}
hn : n < Module.rank R M
⊢ ∃ s, #↑s = n ∧ LinearIndepOn R id s

Tactic:
obtain ⟨⟨s, hs⟩, hs'⟩ := exists_lt_of_lt_ciSup' (hn.trans_eq (Module.rank_def R M))

Result:
case intro.mk
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : Cardinal.{v}
hn : n < Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : n < #↑↑⟨s, hs⟩
⊢ ∃ s, #↑s = n ∧ LinearIndepOn R id s

Proof state:
case intro.mk
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : Cardinal.{v}
hn : n < Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : n < #↑↑⟨s, hs⟩
⊢ ∃ s, #↑s = n ∧ LinearIndepOn R id s

Tactic:
obtain ⟨t, ht, ht'⟩ := le_mk_iff_exists_subset.mp hs'.le

Result:
case intro.mk.intro.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : Cardinal.{v}
hn : n < Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : n < #↑↑⟨s, hs⟩
t : Set M
ht : t ⊆ ↑⟨s, hs⟩
ht' : #↑t = n
⊢ ∃ s, #↑s = n ∧ LinearIndepOn R id s

Proof state:
case intro.mk.intro.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : Cardinal.{v}
hn : n < Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : n < #↑↑⟨s, hs⟩
t : Set M
ht : t ⊆ ↑⟨s, hs⟩
ht' : #↑t = n
⊢ ∃ s, #↑s = n ∧ LinearIndepOn R id s

Tactic:
exact ⟨t, ht', hs.mono ht⟩

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem forall₃_true_iff {β : α → Sort*} {γ : ∀ a, β a → Sort*} :
    (∀ (a) (b : β a), γ a b → True) ↔ True

Proof state:
α : Sort u_1
β : α → Sort u_3
γ : (a : α) → β a → Sort u_4
⊢ (∀ (a : α) (b : β a), γ a b → True) ↔ True

Tactic:
simp

Result:
no goals