harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/Permanent.lean
theorem permanent_updateCol_smul (M : Matrix n n R) (j : n) (c : R) (u : n → R) :
    permanent (updateCol M j <| c • u) = c * permanent (updateCol M j u)

Proof state:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
p : Perm n
i : n
hi : i ∈ univ.erase j
⊢ M.updateCol j (c • u) (p i) i = M.updateCol j u (p i) i

Tactic:
simp only [ne_eq, ne_of_mem_erase hi, not_false_eq_true, updateCol_ne]

Result:
no goals

Proof state:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
⊢ ∑ x : Perm n, c * u (x j) * ∏ i ∈ univ.erase j, M.updateCol j (c • u) (x i) i =
    ∑ x : Perm n, c * u (x j) * ∏ i ∈ univ.erase j, M.updateCol j u (x i) i

Tactic:
congr 1 with p

Result:
case e_f.h
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
p : Perm n
⊢ c * u (p j) * ∏ i ∈ univ.erase j, M.updateCol j (c • u) (p i) i =
    c * u (p j) * ∏ i ∈ univ.erase j, M.updateCol j u (p i) i

Proof state:
case e_f.h
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
p : Perm n
⊢ c * u (p j) * ∏ i ∈ univ.erase j, M.updateCol j (c • u) (p i) i =
    c * u (p j) * ∏ i ∈ univ.erase j, M.updateCol j u (p i) i

Tactic:
rw [Finset.prod_congr rfl (fun i hi ↦ ?_)]

Result:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
p : Perm n
i : n
hi : i ∈ univ.erase j
⊢ M.updateCol j (c • u) (p i) i = M.updateCol j u (p i) i

Proof state:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
⊢ (M.updateCol j (c • u)).permanent = c * (M.updateCol j u).permanent

Tactic:
simp only [permanent, ← mul_prod_erase _ _ (mem_univ j), updateCol_self, Pi.smul_apply,
  smul_eq_mul, mul_sum, ← mul_assoc]

Result:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
M : Matrix n n R
j : n
c : R
u : n → R
⊢ ∑ x : Perm n, c * u (x j) * ∏ i ∈ univ.erase j, M.updateCol j (c • u) (x i) i =
    ∑ x : Perm n, c * u (x j) * ∏ i ∈ univ.erase j, M.updateCol j u (x i) i
-- Mathlib/Data/Bool/Basic.lean
theorem and_eq_false_eq_eq_false_or_eq_false (a b : Bool) :
    ((a && b) = false) = (a = false ∨ b = false)

Proof state:
a b : Bool
⊢ ((a && b) = false) = (a = false ∨ b = false)

Tactic:
cases a <;> cases b <;> simp

Result:
no goals
-- Mathlib/RingTheory/Finiteness/Basic.lean
theorem _root_.LinearMap.finite_iff_of_bijective (f : M →ₛₗ[σ] P) (hf : Function.Bijective f) :
    Module.Finite R M ↔ Module.Finite S P :=
  ⟨fun _ ↦ of_surjective f hf.surjective, fun _ ↦ ⟨fg_of_fg_map_injective f hf.injective <| by
    rwa [Submodule.map_top, LinearMap.range_eq_top.2 hf.surjective, ← Module.finite_def]⟩⟩

Proof state:
R : Type u_1
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_7
P : Type u_6
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Bijective ⇑f
x✝ : Module.Finite S P
⊢ (map f ⊤).FG

Tactic:
rwa [Submodule.map_top, LinearMap.range_eq_top.2 hf.surjective, ← Module.finite_def]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem erase_subset_iff_of_mem (h : a ∈ t) : s.erase a ⊆ t ↔ s ⊆ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : a ∈ t
⊢ s.erase a ⊆ t ↔ s ⊆ t

Tactic:
rw [← subset_insert_iff, insert_eq_of_mem h]

Result:
no goals
-- Mathlib/Data/Matroid/Rank/Cardinal.lean
theorem cRk_insert_closure_eq : M.cRk (insert e (M.closure X)) = M.cRk (insert e X)

Proof state:
α : Type u
M : Matroid α
inst✝ : M.InvariantCardinalRank
e : α
X : Set α
⊢ M.cRk (insert e (M.closure X)) = M.cRk (insert e X)

Tactic:
rw [← union_singleton, cRk_union_closure_left_eq, union_singleton]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Types.lean
theorem pi_lift_π_apply' {β : Type v} (f : β → Type v) {P : Type v}
    (s : ∀ b, P ⟶ f b) (b : β) (x : P) :
    (Pi.π f b : (piObj f) → f b) (@Pi.lift β _ _ f _ P s x) = s b x

Proof state:
β : Type v
f : β → Type v
P : Type v
s : (b : β) → P ⟶ f b
b : β
x : P
⊢ Pi.π f b (Pi.lift s x) = s b x

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem memLp_top_const (c : E) : MemLp (fun _ : α => c) ∞ μ :=
  ⟨aestronglyMeasurable_const, by by_cases h : μ = 0 <;> simp [eLpNorm_const _, h]⟩

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
c : E
⊢ eLpNorm (fun x => c) ⊤ μ < ⊤

Tactic:
by_cases h : μ = 0 <;> simp [eLpNorm_const _, h]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Defs.lean
theorem prod_hom_rel (s : Multiset ι) {r : α → β → Prop} {f : ι → α} {g : ι → β}
    (h₁ : r 1 1) (h₂ : ∀ ⦃a b c⦄, r b c → r (f a * b) (g a * c)) :
    r (s.map f).prod (s.map g).prod :=
  Quotient.inductionOn s fun l => by
    simp only [l.prod_hom_rel h₁ h₂, quot_mk_to_coe, map_coe, prod_coe]

Proof state:
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
s : Multiset ι
r : α → β → Prop
f : ι → α
g : ι → β
h₁ : r 1 1
h₂ : ∀ ⦃a : ι⦄ ⦃b : α⦄ ⦃c : β⦄, r b c → r (f a * b) (g a * c)
l : List ι
⊢ r (map f ⟦l⟧).prod (map g ⟦l⟧).prod

Tactic:
simp only [l.prod_hom_rel h₁ h₂, quot_mk_to_coe, map_coe, prod_coe]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
lemma filter_and_not (s : Finset α) (p q : α → Prop) [DecidablePred p] [DecidablePred q] :
    s.filter (fun a ↦ p a ∧ ¬ q a) = s.filter p \ s.filter q

Proof state:
α : Type u_1
inst✝² : DecidableEq α
s : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ filter (fun a => p a ∧ ¬q a) s = filter p s \ filter q s

Tactic:
rw [filter_and, filter_not, ← inter_sdiff_assoc, inter_eq_left.2 (filter_subset _ _)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/AdditionalOperations.lean
theorem WF.filterMap [BEq α] [Hashable α] {m : Raw α β} (h : m.WF)
    {f : (a : α) → β a → Option (δ a)} : (m.filterMap f).WF

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
h : m.WF
f : (a : α) → β a → Option (δ a)
⊢ (Raw.filterMap f m).WF

Tactic:
simpa only [filterMap_eq h] using
  .wf (Raw₀.filterMap f ⟨m, h.size_buckets_pos⟩).2 (Raw₀.wfImp_filterMap (WF.out h))

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem Const.getDₘ_eq_getValueD [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α]
    {m : Raw₀ α (fun _ => β)} (hm : Raw.WFImp m.1) {a : α} {fallback : β} :
    Const.getDₘ m a fallback = getValueD a (toListModel m.1.buckets) fallback

Proof state:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
hm : Raw.WFImp m.val
a : α
fallback : β
⊢ getDₘ m a fallback = getValueD a (toListModel m.val.buckets) fallback

Tactic:
rw [getDₘ, get?ₘ_eq_getValue? hm, List.getValueD_eq_getValue?]

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Basic.lean
theorem ContMDiffWithinAt.comp_of_eq {t : Set M'} {g : M' → M''} {x : M} {y : M'}
    (hg : ContMDiffWithinAt I' I'' n g t y) (hf : ContMDiffWithinAt I I' n f s x)
    (st : MapsTo f s t) (hx : f x = y) : ContMDiffWithinAt I I'' n (g ∘ f) s x

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
E' : Type u_5
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁷ : TopologicalSpace M'
E'' : Type u_8
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝³ : TopologicalSpace M''
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H'' M''
f : M → M'
s : Set M
n : WithTop ℕ∞
t : Set M'
g : M' → M''
x : M
y : M'
hg : ContMDiffWithinAt I' I'' n g t y
hf : ContMDiffWithinAt I I' n f s x
st : MapsTo f s t
hx : f x = y
⊢ ContMDiffWithinAt I I'' n (g ∘ f) s x

Tactic:
subst hx

Result:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
E' : Type u_5
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁷ : TopologicalSpace M'
E'' : Type u_8
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝³ : TopologicalSpace M''
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H'' M''
f : M → M'
s : Set M
n : WithTop ℕ∞
t : Set M'
g : M' → M''
x : M
hf : ContMDiffWithinAt I I' n f s x
st : MapsTo f s t
hg : ContMDiffWithinAt I' I'' n g t (f x)
⊢ ContMDiffWithinAt I I'' n (g ∘ f) s x

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
E' : Type u_5
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁸ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁷ : TopologicalSpace M'
E'' : Type u_8
inst✝⁶ : NormedAddCommGroup E''
inst✝⁵ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝⁴ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝³ : TopologicalSpace M''
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H'' M''
f : M → M'
s : Set M
n : WithTop ℕ∞
t : Set M'
g : M' → M''
x : M
hf : ContMDiffWithinAt I I' n f s x
st : MapsTo f s t
hg : ContMDiffWithinAt I' I'' n g t (f x)
⊢ ContMDiffWithinAt I I'' n (g ∘ f) s x

Tactic:
exact hg.comp x hf st

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem sigma_one_apply (n : ℕ) : σ 1 n = ∑ d ∈ divisors n, d

Proof state:
n : ℕ
⊢ (σ 1) n = ∑ d ∈ n.divisors, d

Tactic:
simp [sigma_apply]

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_map (f : E[X]) (i : E →+* K) : (f.map i).natSepDegree = f.natSepDegree

Proof state:
E : Type v
inst✝¹ : Field E
K : Type w
inst✝ : Field K
f : E[X]
i : E →+* K
x✝ : Algebra E K := i.toAlgebra
⊢ (map i f).natSepDegree = f.natSepDegree

Tactic:
simp_rw [show i = algebraMap E K by rfl, natSepDegree_eq_of_isAlgClosed (AlgebraicClosure K),
  aroots_def, map_map, ← IsScalarTower.algebraMap_eq]

Result:
no goals

Proof state:
E : Type v
inst✝¹ : Field E
K : Type w
inst✝ : Field K
f : E[X]
i : E →+* K
⊢ (map i f).natSepDegree = f.natSepDegree

Tactic:
let _ := i.toAlgebra

Result:
E : Type v
inst✝¹ : Field E
K : Type w
inst✝ : Field K
f : E[X]
i : E →+* K
x✝ : Algebra E K := i.toAlgebra
⊢ (map i f).natSepDegree = f.natSepDegree

Proof state:
E : Type v
inst✝¹ : Field E
K : Type w
inst✝ : Field K
f : E[X]
i : E →+* K
⊢ (map i f).natSepDegree = f.natSepDegree

Tactic:
classical
let _ := i.toAlgebra
simp_rw [show i = algebraMap E K by rfl, natSepDegree_eq_of_isAlgClosed (AlgebraicClosure K),
  aroots_def, map_map, ← IsScalarTower.algebraMap_eq]

Result:
no goals

Proof state:
E : Type v
inst✝¹ : Field E
K : Type w
inst✝ : Field K
f : E[X]
i : E →+* K
x✝ : Algebra E K := i.toAlgebra
⊢ i = algebraMap E K

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Localization/HomEquiv.lean
@[simp]
lemma homEquiv_id : homEquiv W L₁ L₂ (𝟙 (L₁.obj X)) = 𝟙 (L₂.obj X)

Proof state:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst✝⁴ : Category.{u_9, u_1} C
inst✝³ : Category.{u_10, u_5} D₁
inst✝² : Category.{u_8, u_6} D₂
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝¹ : L₁.IsLocalization W
L₂ : C ⥤ D₂
inst✝ : L₂.IsLocalization W
X : C
⊢ (homEquiv W L₁ L₂) (𝟙 (L₁.obj X)) = 𝟙 (L₂.obj X)

Tactic:
simp [homEquiv_apply]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean
theorem Cover.iUnion_range {X : Scheme.{u}} (𝒰 : X.Cover P) :
    ⋃ i, Set.range (𝒰.map i).base = Set.univ

Proof state:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover P X
x : ↑↑X.toPresheafedSpace
⊢ ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (𝒰.map i).base)

Tactic:
exact ⟨𝒰.f x, 𝒰.covers x⟩

Result:
no goals

Proof state:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover P X
⊢ ⋃ i, Set.range ⇑(ConcreteCategory.hom (𝒰.map i).base) = Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]

Result:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover P X
⊢ ∀ (x : ↑↑X.toPresheafedSpace), x ∈ ⋃ i, Set.range ⇑(ConcreteCategory.hom (𝒰.map i).base)

Proof state:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover P X
⊢ ∀ (x : ↑↑X.toPresheafedSpace), x ∈ ⋃ i, Set.range ⇑(ConcreteCategory.hom (𝒰.map i).base)

Tactic:
intro x

Result:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover P X
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ⋃ i, Set.range ⇑(ConcreteCategory.hom (𝒰.map i).base)

Proof state:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover P X
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ⋃ i, Set.range ⇑(ConcreteCategory.hom (𝒰.map i).base)

Tactic:
rw [Set.mem_iUnion]

Result:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover P X
x : ↑↑X.toPresheafedSpace
⊢ ∃ i, x ∈ Set.range ⇑(ConcreteCategory.hom (𝒰.map i).base)
-- Mathlib/Data/Nat/Dist.lean
theorem dist_mul_right (n k m : ℕ) : dist (n * k) (m * k) = dist n m * k

Proof state:
n k m : ℕ
⊢ (n * k).dist (m * k) = n.dist m * k

Tactic:
rw [dist, dist, right_distrib, tsub_mul n, tsub_mul m]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Operations.lean
theorem coe_iSup {ι} (f : ι → OuterMeasure α) : ⇑(⨆ i, f i) = ⨆ i, ⇑(f i) :=
  funext fun s => by simp

Proof state:
α : Type u_1
ι : Sort u_3
f : ι → OuterMeasure α
s : Set α
⊢ (⨆ i, f i) s = (⨆ i, ⇑(f i)) s

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
@[simp] lemma insert_subset_insert_iff (ha : a ∉ s) : insert a s ⊆ insert a t ↔ s ⊆ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
⊢ ↑(insert a s) ⊆ ↑(insert a t) ↔ ↑s ⊆ ↑t

Tactic:
simp [-coe_subset, ha]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
⊢ insert a s ⊆ insert a t ↔ s ⊆ t

Tactic:
simp_rw [← coe_subset]

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
⊢ ↑(insert a s) ⊆ ↑(insert a t) ↔ ↑s ⊆ ↑t
-- Mathlib/Logic/Relation.lean
theorem ReflTransGen.lift' {p : β → β → Prop} {a b : α} (f : α → β)
    (h : ∀ a b, r a b → ReflTransGen p (f a) (f b))
    (hab : ReflTransGen r a b) : ReflTransGen p (f a) (f b)

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
a b : α
f : α → β
h : ∀ (a b : α), r a b → ReflTransGen p (f a) (f b)
hab : ReflTransGen r a b
⊢ ReflTransGen p (f a) (f b)

Tactic:
simpa [reflTransGen_idem] using hab.lift f h

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma div_ne_zero_iff_of_dvd (hba : b ∣ a) : a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0

Proof state:
a b : ℕ
hba : b ∣ a
⊢ a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0

Tactic:
obtain rfl | hb := Decidable.em (b = 0) <;>
  simp [Nat.div_ne_zero_iff, Nat.le_iff_ne_zero_of_dvd, *]

Result:
no goals
-- Mathlib/RingTheory/Localization/BaseChange.lean
lemma Algebra.isPushout_of_isLocalization [IsLocalization (Algebra.algebraMapSubmonoid T S) B] :
    Algebra.IsPushout R T A B

Proof state:
R : Type u_1
inst✝¹² : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹¹ : CommSemiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : IsLocalization S A
T : Type u_5
B : Type u_6
inst✝⁸ : CommSemiring T
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra T B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R T B
inst✝¹ : IsScalarTower R A B
inst✝ : IsLocalization (algebraMapSubmonoid T S) B
⊢ IsBaseChange A (IsScalarTower.toAlgHom R T B).toLinearMap

Tactic:
apply IsLocalizedModule.isBaseChange S

Result:
no goals

Proof state:
R : Type u_1
inst✝¹² : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹¹ : CommSemiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : IsLocalization S A
T : Type u_5
B : Type u_6
inst✝⁸ : CommSemiring T
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra T B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R T B
inst✝¹ : IsScalarTower R A B
inst✝ : IsLocalization (algebraMapSubmonoid T S) B
⊢ IsPushout R T A B

Tactic:
rw [Algebra.IsPushout.comm, Algebra.isPushout_iff]

Result:
R : Type u_1
inst✝¹² : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹¹ : CommSemiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : IsLocalization S A
T : Type u_5
B : Type u_6
inst✝⁸ : CommSemiring T
inst✝⁷ : CommSemiring B
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra T B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R T B
inst✝¹ : IsScalarTower R A B
inst✝ : IsLocalization (algebraMapSubmonoid T S) B
⊢ IsBaseChange A (IsScalarTower.toAlgHom R T B).toLinearMap
-- Mathlib/Analysis/Convex/Strict.lean
theorem StrictConvex.mem_smul_of_zero_mem (hs : StrictConvex 𝕜 s) (zero_mem : (0 : E) ∈ s)
    (hx : x ∈ s) (hx₀ : x ≠ 0) {t : 𝕜} (ht : 1 < t) : x ∈ t • interior s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hs : StrictConvex 𝕜 s
zero_mem : 0 ∈ s
hx : x ∈ s
hx₀ : x ≠ 0
t : 𝕜
ht : 1 < t
⊢ x ∈ t • interior s

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ (by positivity)]

Result:
𝕜 : Type u_1
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hs : StrictConvex 𝕜 s
zero_mem : 0 ∈ s
hx : x ∈ s
hx₀ : x ≠ 0
t : 𝕜
ht : 1 < t
⊢ t⁻¹ • x ∈ interior s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hs : StrictConvex 𝕜 s
zero_mem : 0 ∈ s
hx : x ∈ s
hx₀ : x ≠ 0
t : 𝕜
ht : 1 < t
⊢ t ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hs : StrictConvex 𝕜 s
zero_mem : 0 ∈ s
hx : x ∈ s
hx₀ : x ≠ 0
t : 𝕜
ht : 1 < t
⊢ t⁻¹ • x ∈ interior s

Tactic:
exact hs.smul_mem_of_zero_mem zero_mem hx hx₀ (by positivity) (inv_lt_one_of_one_lt₀ ht)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hs : StrictConvex 𝕜 s
zero_mem : 0 ∈ s
hx : x ∈ s
hx₀ : x ≠ 0
t : 𝕜
ht : 1 < t
⊢ 0 < t⁻¹

Tactic:
positivity

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_neg_uIcc : -[[a, b]] = [[-a, -b]]

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
⊢ -[[a, b]] = [[-a, -b]]

Tactic:
simp only [← Icc_min_max, neg_Icc, min_neg_neg, max_neg_neg]

Result:
no goals
-- Mathlib/Topology/ExtremallyDisconnected.lean
theorem extremallyDisconnected_of_homeo {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    [ExtremallyDisconnected X] (e : X ≃ₜ Y) : ExtremallyDisconnected Y where
  open_closure U hU

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ExtremallyDisconnected X
e : X ≃ₜ Y
U : Set Y
hU : IsOpen U
⊢ IsOpen (closure (⇑e.symm '' U))

Tactic:
exact ExtremallyDisconnected.open_closure _ (e.symm.isOpen_image.mpr hU)

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ExtremallyDisconnected X
e : X ≃ₜ Y
U : Set Y
hU : IsOpen U
⊢ IsOpen (closure U)

Tactic:
rw [e.symm.isInducing.closure_eq_preimage_closure_image, Homeomorph.isOpen_preimage]

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : ExtremallyDisconnected X
e : X ≃ₜ Y
U : Set Y
hU : IsOpen U
⊢ IsOpen (closure (⇑e.symm '' U))
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem data_join (ss : List String) : (join ss).data = (ss.map data).flatten

Proof state:
ss : List String
⊢ (join ss).data = (List.map data ss).flatten

Tactic:
rw [join_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem add_neg_emod_self (a b : Int) : (a + -b) % b = a % b

Proof state:
a b : Int
⊢ (a + -b) % b = a % b

Tactic:
rw [← Int.sub_eq_add_neg, emod_sub_cancel]

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
theorem count_erase_self (a : α) (s : Multiset α) : count a (erase s a) = count a s - 1 :=
  Quotient.inductionOn s fun l => by
    convert List.count_erase_self a l <;> rw [← coe_count] <;> simp

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ a) = count a ⟦l⟧ - 1

Tactic:
convert List.count_erase_self a l <;> rw [← coe_count] <;> simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem le_mul_left (a : Ordinal) {b : Ordinal} (hb : 0 < b) : a ≤ a * b

Proof state:
case h.e'_3
a b : Ordinal.{u_4}
hb : 0 < b
⊢ a = a * 1

Tactic:
rw [mul_one a]

Result:
no goals

Proof state:
a b : Ordinal.{u_4}
hb : 0 < b
⊢ a ≤ a * b

Tactic:
convert mul_le_mul_left' (one_le_iff_pos.2 hb) a

Result:
case h.e'_3
a b : Ordinal.{u_4}
hb : 0 < b
⊢ a = a * 1
-- Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
lemma yoneda_exact₂ {X : C} (f : T.obj₂ ⟶ X) (hf : T.mor₁ ≫ f = 0) :
    ∃ (g : T.obj₃ ⟶ X), f = T.mor₂ ≫ g

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : T.obj₂ ⟶ X
hf : T.mor₁ ≫ f = 0
g : T.obj₃ ⟶ (mk 0 (𝟙 X) 0).obj₃
hg₁ : T.mor₂ ≫ g = f ≫ (mk 0 (𝟙 X) 0).mor₂
right✝ : T.mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map 0 = g ≫ (mk 0 (𝟙 X) 0).mor₃
⊢ f = T.mor₂ ≫ g

Tactic:
simpa using hg₁.symm

Result:
no goals

Proof state:
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : T.obj₂ ⟶ X
hf : T.mor₁ ≫ f = 0
g : T.obj₃ ⟶ (mk 0 (𝟙 X) 0).obj₃
hg₁ : T.mor₂ ≫ g = f ≫ (mk 0 (𝟙 X) 0).mor₂
right✝ : T.mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map 0 = g ≫ (mk 0 (𝟙 X) 0).mor₃
⊢ ∃ g, f = T.mor₂ ≫ g

Tactic:
exact ⟨g, by simpa using hg₁.symm⟩

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : T.obj₂ ⟶ X
hf : T.mor₁ ≫ f = 0
⊢ ∃ g, f = T.mor₂ ≫ g

Tactic:
obtain ⟨g, ⟨hg₁, _⟩⟩ := complete_distinguished_triangle_morphism T _ hT
  (contractible_distinguished₁ X) 0 f (by aesop_cat)

Result:
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : T.obj₂ ⟶ X
hf : T.mor₁ ≫ f = 0
g : T.obj₃ ⟶ (mk 0 (𝟙 X) 0).obj₃
hg₁ : T.mor₂ ≫ g = f ≫ (mk 0 (𝟙 X) 0).mor₂
right✝ : T.mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map 0 = g ≫ (mk 0 (𝟙 X) 0).mor₃
⊢ ∃ g, f = T.mor₂ ≫ g

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : T.obj₂ ⟶ X
hf : T.mor₁ ≫ f = 0
⊢ T.mor₁ ≫ f = 0 ≫ (mk 0 (𝟙 X) 0).mor₁

Tactic:
aesop_cat

Result:
no goals