harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/Relrank.lean
theorem rank_bot_mul_relrank (h : A ≤ B) : Module.rank F A * relrank A B = Module.rank F B

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
h : A ≤ B
⊢ Module.rank F ↥A * A.relrank B = Module.rank F ↥B

Tactic:
rw [relrank_eq_rank_of_le h]

Result:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
h : A ≤ B
⊢ Module.rank F ↥A * Module.rank ↥A ↥(extendScalars h) = Module.rank F ↥B

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
h : A ≤ B
⊢ Module.rank F ↥A * Module.rank ↥A ↥(extendScalars h) = Module.rank F ↥B

Tactic:
letI : Algebra A B := (inclusion h).toAlgebra

Result:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
h : A ≤ B
this : Algebra ↥A ↥B := (inclusion h).toAlgebra
⊢ Module.rank F ↥A * Module.rank ↥A ↥(extendScalars h) = Module.rank F ↥B

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
h : A ≤ B
this✝ : Algebra ↥A ↥B := (inclusion h).toAlgebra
this : IsScalarTower F ↥A ↥B
⊢ Module.rank F ↥A * Module.rank ↥A ↥(extendScalars h) = Module.rank F ↥B

Tactic:
exact rank_mul_rank F A B

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
h : A ≤ B
this : Algebra ↥A ↥B := (inclusion h).toAlgebra
⊢ Module.rank F ↥A * Module.rank ↥A ↥(extendScalars h) = Module.rank F ↥B

Tactic:
haveI : IsScalarTower F A B := IsScalarTower.of_algebraMap_eq' rfl

Result:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
h : A ≤ B
this✝ : Algebra ↥A ↥B := (inclusion h).toAlgebra
this : IsScalarTower F ↥A ↥B
⊢ Module.rank F ↥A * Module.rank ↥A ↥(extendScalars h) = Module.rank F ↥B
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem getThenInsertIfNew?_fst_eq [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} (h : m.WF)
    {a : α} {b : β a} : (m.getThenInsertIfNew? a b).1 =
      (Raw₀.getThenInsertIfNew? ⟨m, h.size_buckets_pos⟩ a b).1

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw α β
h : m.WF
a : α
b : β a
⊢ (m.getThenInsertIfNew? a b).fst = (Raw₀.getThenInsertIfNew? ⟨m, ⋯⟩ a b).fst

Tactic:
simp [Raw.getThenInsertIfNew?, h.size_buckets_pos]

Result:
no goals
-- Mathlib/Order/WellFoundedSet.lean
theorem PartiallyWellOrderedOn.image_of_monotone_on (hs : s.PartiallyWellOrderedOn r)
    (hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)) : (f '' s).PartiallyWellOrderedOn r'

Proof state:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : s.PartiallyWellOrderedOn r
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
g' : ℕ → β
hg' : ∀ (n : ℕ), g' n ∈ f '' s
⊢ ∃ m n, m < n ∧ r' (g' m) (g' n)

Tactic:
choose g hgs heq using hg'

Result:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : s.PartiallyWellOrderedOn r
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
g' : ℕ → β
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = g' n
⊢ ∃ m n, m < n ∧ r' (g' m) (g' n)

Proof state:
case intro.intro.intro
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : s.PartiallyWellOrderedOn r
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = (f ∘ g) n
m n : ℕ
hlt : m < n
hmn : r (g m) (g n)
⊢ ∃ m n, m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)

Tactic:
exact ⟨m, n, hlt, hf _ (hgs m) _ (hgs n) hmn⟩

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : s.PartiallyWellOrderedOn r
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
g' : ℕ → β
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = g' n
⊢ ∃ m n, m < n ∧ r' (g' m) (g' n)

Tactic:
obtain rfl : f ∘ g = g' := funext heq

Result:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : s.PartiallyWellOrderedOn r
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = (f ∘ g) n
⊢ ∃ m n, m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)

Proof state:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : s.PartiallyWellOrderedOn r
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = (f ∘ g) n
⊢ ∃ m n, m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)

Tactic:
obtain ⟨m, n, hlt, hmn⟩ := hs g hgs

Result:
case intro.intro.intro
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : s.PartiallyWellOrderedOn r
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = (f ∘ g) n
m n : ℕ
hlt : m < n
hmn : r (g m) (g n)
⊢ ∃ m n, m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)

Proof state:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : s.PartiallyWellOrderedOn r
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
⊢ (f '' s).PartiallyWellOrderedOn r'

Tactic:
intro g' hg'

Result:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : s.PartiallyWellOrderedOn r
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
g' : ℕ → β
hg' : ∀ (n : ℕ), g' n ∈ f '' s
⊢ ∃ m n, m < n ∧ r' (g' m) (g' n)
-- Mathlib/Order/Category/Frm.lean
lemma hom_inv_apply {X Y : Frm} (e : X ≅ Y) (s : Y) : e.hom (e.inv s) = s

Proof state:
X Y : Frm
e : X ≅ Y
s : ↑Y
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem iff_ne_zero [MonoidWithZero R] {f : ArithmeticFunction R} :
    IsMultiplicative f ↔
      f 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n

Proof state:
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
⊢ f.IsMultiplicative ↔ f 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n

Tactic:
refine and_congr_right' (forall₂_congr fun m n => ⟨fun h _ _ => h, fun h hmn => ?_⟩)

Result:
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m n : ℕ
h : m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n
hmn : m.Coprime n
⊢ f (m * n) = f m * f n

Proof state:
case inr
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m n : ℕ
h : m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n
hmn : m.Coprime n
hm : m ≠ 0
⊢ f (m * n) = f m * f n

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Result:
case inr.inl
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m : ℕ
hm : m ≠ 0
h : m ≠ 0 → 0 ≠ 0 → m.Coprime 0 → f (m * 0) = f m * f 0
hmn : m.Coprime 0
⊢ f (m * 0) = f m * f 0

case inr.inr
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m n : ℕ
h : m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n
hmn : m.Coprime n
hm : m ≠ 0
hn : n ≠ 0
⊢ f (m * n) = f m * f n

Proof state:
case inr.inr
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m n : ℕ
h : m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n
hmn : m.Coprime n
hm : m ≠ 0
hn : n ≠ 0
⊢ f (m * n) = f m * f n

Tactic:
exact h hm hn hmn

Result:
no goals

Proof state:
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m n : ℕ
h : m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n
hmn : m.Coprime n
⊢ f (m * n) = f m * f n

Tactic:
rcases eq_or_ne m 0 with (rfl | hm)

Result:
case inl
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
n : ℕ
h : 0 ≠ 0 → n ≠ 0 → Coprime 0 n → f (0 * n) = f 0 * f n
hmn : Coprime 0 n
⊢ f (0 * n) = f 0 * f n

case inr
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m n : ℕ
h : m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n
hmn : m.Coprime n
hm : m ≠ 0
⊢ f (m * n) = f m * f n

Proof state:
case inr.inl
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
m : ℕ
hm : m ≠ 0
h : m ≠ 0 → 0 ≠ 0 → m.Coprime 0 → f (m * 0) = f m * f 0
hmn : m.Coprime 0
⊢ f (m * 0) = f m * f 0

Tactic:
simp

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝ : MonoidWithZero R
f : ArithmeticFunction R
n : ℕ
h : 0 ≠ 0 → n ≠ 0 → Coprime 0 n → f (0 * n) = f 0 * f n
hmn : Coprime 0 n
⊢ f (0 * n) = f 0 * f n

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fintype/EquivFin.lean
theorem Finset.exists_minimal {α : Type*} [Preorder α] (s : Finset α) (h : s.Nonempty) :
    ∃ m ∈ s, ∀ x ∈ s, ¬x < m

Proof state:
case intro
α : Type u_4
inst✝ : Preorder α
s : Finset α
c : α
hcs : c ∈ s
⊢ ∃ m ∈ s, ∀ x ∈ s, ¬x < m

Tactic:
have : WellFounded (@LT.lt { x // x ∈ s } _) := Finite.wellFounded_of_trans_of_irrefl _

Result:
case intro
α : Type u_4
inst✝ : Preorder α
s : Finset α
c : α
hcs : c ∈ s
this : WellFounded LT.lt
⊢ ∃ m ∈ s, ∀ x ∈ s, ¬x < m

Proof state:
case intro
α : Type u_4
inst✝ : Preorder α
s : Finset α
c : α
hcs : c ∈ s
this : WellFounded LT.lt
⊢ ∃ m ∈ s, ∀ x ∈ s, ¬x < m

Tactic:
obtain ⟨⟨m, hms : m ∈ s⟩, -, H⟩ := this.has_min Set.univ ⟨⟨c, hcs⟩, trivial⟩

Result:
case intro.intro.mk.intro
α : Type u_4
inst✝ : Preorder α
s : Finset α
c : α
hcs : c ∈ s
this : WellFounded LT.lt
m : α
hms : m ∈ s
H : ∀ x ∈ Set.univ, ¬x < ⟨m, hms⟩
⊢ ∃ m ∈ s, ∀ x ∈ s, ¬x < m

Proof state:
α : Type u_4
inst✝ : Preorder α
s : Finset α
h : s.Nonempty
⊢ ∃ m ∈ s, ∀ x ∈ s, ¬x < m

Tactic:
obtain ⟨c, hcs : c ∈ s⟩ := h

Result:
case intro
α : Type u_4
inst✝ : Preorder α
s : Finset α
c : α
hcs : c ∈ s
⊢ ∃ m ∈ s, ∀ x ∈ s, ¬x < m

Proof state:
case intro.intro.mk.intro
α : Type u_4
inst✝ : Preorder α
s : Finset α
c : α
hcs : c ∈ s
this : WellFounded LT.lt
m : α
hms : m ∈ s
H : ∀ x ∈ Set.univ, ¬x < ⟨m, hms⟩
⊢ ∃ m ∈ s, ∀ x ∈ s, ¬x < m

Tactic:
exact ⟨m, hms, fun x hx hxm => H ⟨x, hx⟩ trivial hxm⟩

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem inv_zero : (0 : Rat).inv = 0

Proof state:
⊢ (if h : num 0 < 0 then { num := -↑(den 0), den := (num 0).natAbs, den_nz := ⋯, reduced := ⋯ }
    else if h : num 0 > 0 then { num := ↑(den 0), den := (num 0).natAbs, den_nz := ⋯, reduced := ⋯ } else 0) =
    0

Tactic:
rfl

Result:
no goals

Proof state:
⊢ Rat.inv 0 = 0

Tactic:
unfold Rat.inv

Result:
⊢ (if h : num 0 < 0 then { num := -↑(den 0), den := (num 0).natAbs, den_nz := ⋯, reduced := ⋯ }
    else if h : num 0 > 0 then { num := ↑(den 0), den := (num 0).natAbs, den_nz := ⋯, reduced := ⋯ } else 0) =
    0
-- Mathlib/AlgebraicTopology/SimplicialNerve.lean
@[simp]
lemma id_comp (i j : SimplicialThickening J) :
    (λ_ (Hom i j)).inv ≫ id i ▷ Hom i j ≫ comp i i j = 𝟙 (Hom i j)

Proof state:
J : Type u_1
inst✝ : LinearOrder J
i j : SimplicialThickening J
⊢ id i ▷ Hom i j ≫ comp i i j = (λ_ (Hom i j)).hom ≫ 𝟙 (Hom i j)

Tactic:
ext

Result:
case w.h
J : Type u_1
inst✝ : LinearOrder J
i j : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
a✝ : (𝟙_ SSet ⊗ Hom i j).obj n✝
⊢ (id i ▷ Hom i j ≫ comp i i j).app n✝ a✝ = ((λ_ (Hom i j)).hom ≫ 𝟙 (Hom i j)).app n✝ a✝

Proof state:
J : Type u_1
inst✝ : LinearOrder J
i j : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
a✝ : (𝟙_ SSet ⊗ Hom i j).obj n✝
x✝ : Fin ((Opposite.unop n✝).len + 1)
⊢ ((id i ▷ Hom i j ≫ comp i i j).app n✝ a✝).obj x✝ = (((λ_ (Hom i j)).hom ≫ 𝟙 (Hom i j)).app n✝ a✝).obj x✝

Tactic:
simp

Result:
no goals

Proof state:
case w.h
J : Type u_1
inst✝ : LinearOrder J
i j : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
a✝ : (𝟙_ SSet ⊗ Hom i j).obj n✝
⊢ (id i ▷ Hom i j ≫ comp i i j).app n✝ a✝ = ((λ_ (Hom i j)).hom ≫ 𝟙 (Hom i j)).app n✝ a✝

Tactic:
exact Functor.ext (fun _ ↦ by simp)

Result:
no goals

Proof state:
J : Type u_1
inst✝ : LinearOrder J
i j : SimplicialThickening J
⊢ (λ_ (Hom i j)).inv ≫ id i ▷ Hom i j ≫ comp i i j = 𝟙 (Hom i j)

Tactic:
rw [Iso.inv_comp_eq]

Result:
J : Type u_1
inst✝ : LinearOrder J
i j : SimplicialThickening J
⊢ id i ▷ Hom i j ≫ comp i i j = (λ_ (Hom i j)).hom ≫ 𝟙 (Hom i j)
-- Mathlib/Data/Finset/Prod.lean
theorem product_image_fst [DecidableEq α] (ht : t.Nonempty) : (s ×ˢ t).image Prod.fst = s

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq α
ht : t.Nonempty
⊢ image Prod.fst (s ×ˢ t) = s

Tactic:
ext i

Result:
case h
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq α
ht : t.Nonempty
i : α
⊢ i ∈ image Prod.fst (s ×ˢ t) ↔ i ∈ s

Proof state:
case h
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq α
ht : t.Nonempty
i : α
⊢ i ∈ image Prod.fst (s ×ˢ t) ↔ i ∈ s

Tactic:
simp [mem_image, ht.exists_mem]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
/-- A variant of `prod_range_succ` which pulls off the first term in the product rather than the
last. -/
@[to_additive
"A variant of `sum_range_succ` which pulls off the first term in the sum rather than the last."]
lemma prod_range_succ' (f : ℕ → M) (n : ℕ) :
    ((range n.succ).map f).prod = f 0 * ((range n).map fun i ↦ f i.succ).prod

Proof state:
M : Type u_4
inst✝ : Monoid M
f : ℕ → M
n : ℕ
⊢ (map f (0 :: map Nat.succ (range n))).prod = f 0 * (map (fun i => f i.succ) (range n)).prod

Tactic:
simp [Function.comp_def]

Result:
no goals

Proof state:
M : Type u_4
inst✝ : Monoid M
f : ℕ → M
n : ℕ
⊢ (map f (range n.succ)).prod = f 0 * (map (fun i => f i.succ) (range n)).prod

Tactic:
rw [range_succ_eq_map]

Result:
M : Type u_4
inst✝ : Monoid M
f : ℕ → M
n : ℕ
⊢ (map f (0 :: map Nat.succ (range n))).prod = f 0 * (map (fun i => f i.succ) (range n)).prod
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_lt_eq (absorbs : Absorbent ℝ s) (a : ℝ) :
    { x | gauge s x < a } = ⋃ r ∈ Set.Ioo 0 (a : ℝ), r • s

Proof state:
case h
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
absorbs : Absorbent ℝ s
a : ℝ
x✝ : E
⊢ gauge s x✝ < a ↔ ∃ i, 0 < i ∧ i < a ∧ x✝ ∈ i • s

Tactic:
exact
  ⟨exists_lt_of_gauge_lt absorbs, fun ⟨r, hr₀, hr₁, hx⟩ =>
    (gauge_le_of_mem hr₀.le hx).trans_lt hr₁⟩

Result:
no goals

Proof state:
case h
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
absorbs : Absorbent ℝ s
a : ℝ
x✝ : E
⊢ x✝ ∈ {x | gauge s x < a} ↔ x✝ ∈ ⋃ r ∈ Ioo 0 a, r • s

Tactic:
simp_rw [mem_setOf, mem_iUnion, exists_prop, mem_Ioo, and_assoc]

Result:
case h
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
absorbs : Absorbent ℝ s
a : ℝ
x✝ : E
⊢ gauge s x✝ < a ↔ ∃ i, 0 < i ∧ i < a ∧ x✝ ∈ i • s

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
absorbs : Absorbent ℝ s
a : ℝ
⊢ {x | gauge s x < a} = ⋃ r ∈ Ioo 0 a, r • s

Tactic:
ext

Result:
case h
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
absorbs : Absorbent ℝ s
a : ℝ
x✝ : E
⊢ x✝ ∈ {x | gauge s x < a} ↔ x✝ ∈ ⋃ r ∈ Ioo 0 a, r • s
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem ideal_factor_ne_zero {R} [CommRing R] {K : Type*} [Field K] [Algebra R K]
    [IsFractionRing R K] {I : FractionalIdeal R⁰ K} (hI : I ≠ 0) {a : R} {J : Ideal R}
    (haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J) : J ≠ 0 := fun h ↦ by
  rw [h, Ideal.zero_eq_bot, coeIdeal_bot, MulZeroClass.mul_zero] at haJ
  exact hI haJ

Proof state:
R : Type u_6
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
h : J = 0
⊢ False

Tactic:
rw [h, Ideal.zero_eq_bot, coeIdeal_bot, MulZeroClass.mul_zero] at haJ

Result:
R : Type u_6
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = 0
h : J = 0
⊢ False

Proof state:
R : Type u_6
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = 0
h : J = 0
⊢ False

Tactic:
exact hI haJ

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem exists_of_kerase {a : α} {l : List (Sigma β)} (h : a ∈ l.keys) :
    ∃ (b : β a) (l₁ l₂ : List (Sigma β)),
      a ∉ l₁.keys ∧ l = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a l = l₁ ++ l₂

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, a ∉ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
h : a ∈ (hd :: tl).keys
e : ¬a = hd.fst
⊢ ∃ b l₁ l₂, a ∉ l₁.keys ∧ hd :: tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂

Tactic:
simp only [keys_cons, mem_cons] at h

Result:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, a ∉ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a = hd.fst ∨ a ∈ tl.keys
⊢ ∃ b l₁ l₂, a ∉ l₁.keys ∧ hd :: tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, a ∉ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ tl.keys
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : a ∉ tl₁.keys
h₂ : tl = tl₁ ++ ⟨a, b⟩ :: tl₂
h₃ : kerase a tl = tl₁ ++ tl₂
⊢ hd :: tl = hd :: tl₁ ++ ⟨a, b⟩ :: tl₂

Tactic:
rw [h₂]

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, a ∉ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ tl.keys
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : a ∉ tl₁.keys
h₂ : tl = tl₁ ++ ⟨a, b⟩ :: tl₂
h₃ : kerase a tl = tl₁ ++ tl₂
⊢ hd :: (tl₁ ++ ⟨a, b⟩ :: tl₂) = hd :: tl₁ ++ ⟨a, b⟩ :: tl₂

Proof state:
case mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
tl : List (Sigma β)
fst✝ : α
snd✝ : β fst✝
ih :
  ⟨fst✝, snd✝⟩.fst ∈ tl.keys →
    ∃ b l₁ l₂,
      ⟨fst✝, snd✝⟩.fst ∉ l₁.keys ∧ tl = l₁ ++ ⟨⟨fst✝, snd✝⟩.fst, b⟩ :: l₂ ∧ kerase ⟨fst✝, snd✝⟩.fst tl = l₁ ++ l₂
h : ⟨fst✝, snd✝⟩.fst ∈ (⟨fst✝, snd✝⟩ :: tl).keys
⊢ ⟨fst✝, snd✝⟩ :: tl = [] ++ ⟨⟨fst✝, snd✝⟩.fst, ⟨fst✝, snd✝⟩.snd⟩ :: tl

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Group/Conj.lean
theorem mem_carrier_iff_mk_eq {a : α} {b : ConjClasses α} :
    a ∈ carrier b ↔ ConjClasses.mk a = b

Proof state:
α : Type u
inst✝ : Monoid α
a : α
⊢ ∀ (a_1 : α), a ∈ (ConjClasses.mk a_1).carrier ↔ ConjClasses.mk a = ConjClasses.mk a_1

Tactic:
intro b

Result:
α : Type u
inst✝ : Monoid α
a b : α
⊢ a ∈ (ConjClasses.mk b).carrier ↔ ConjClasses.mk a = ConjClasses.mk b

Proof state:
α : Type u
inst✝ : Monoid α
a b : α
⊢ a ∈ (ConjClasses.mk b).carrier ↔ ConjClasses.mk a = ConjClasses.mk b

Tactic:
rw [carrier, eq_comm, mk_eq_mk_iff_isConj, ← quotient_mk_eq_mk, Quotient.lift_mk]

Result:
α : Type u
inst✝ : Monoid α
a b : α
⊢ a ∈ conjugatesOf b ↔ IsConj b a

Proof state:
α : Type u
inst✝ : Monoid α
a b : α
⊢ a ∈ conjugatesOf b ↔ IsConj b a

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
inst✝ : Monoid α
a : α
⊢ ∀ {b : ConjClasses α}, a ∈ b.carrier ↔ ConjClasses.mk a = b

Tactic:
rw [forall_isConj]

Result:
α : Type u
inst✝ : Monoid α
a : α
⊢ ∀ (a_1 : α), a ∈ (ConjClasses.mk a_1).carrier ↔ ConjClasses.mk a = ConjClasses.mk a_1

Proof state:
α : Type u
inst✝ : Monoid α
a : α
b : ConjClasses α
⊢ a ∈ b.carrier ↔ ConjClasses.mk a = b

Tactic:
revert b

Result:
α : Type u
inst✝ : Monoid α
a : α
⊢ ∀ {b : ConjClasses α}, a ∈ b.carrier ↔ ConjClasses.mk a = b
-- Mathlib/Data/List/Perm/Basic.lean
theorem Perm.flatMap_left (l : List α) {f g : α → List β} (h : ∀ a ∈ l, f a ~ g a) :
    l.flatMap f ~ l.flatMap g :=
  Perm.flatten_congr <| by
    rwa [List.forall₂_map_right_iff, List.forall₂_map_left_iff, List.forall₂_same]

Proof state:
α : Type u_1
β : Type u_2
l : List α
f g : α → List β
h : ∀ (a : α), a ∈ l → f a ~ g a
⊢ Forall₂ (fun x1 x2 => x1 ~ x2) (List.map f l) (List.map g l)

Tactic:
rwa [List.forall₂_map_right_iff, List.forall₂_map_left_iff, List.forall₂_same]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L2Space.lean
theorem memLp_two_iff_integrable_sq {f : α → ℝ} (hf : AEStronglyMeasurable f μ) :
    MemLp f 2 μ ↔ Integrable (fun x => f x ^ 2) μ

Proof state:
case h.e'_2.h.e'_6.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
x✝ : α
⊢ f x✝ ^ 2 = ‖f x✝‖ ^ 2

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
⊢ MemLp f 2 μ ↔ Integrable (fun x => f x ^ 2) μ

Tactic:
convert memLp_two_iff_integrable_sq_norm hf using 3

Result:
case h.e'_2.h.e'_6.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
x✝ : α
⊢ f x✝ ^ 2 = ‖f x✝‖ ^ 2
-- Mathlib/Analysis/Analytic/Basic.lean
lemma HasFPowerSeriesAt.hasFPowerSeriesWithinAt (hf : HasFPowerSeriesAt f p x) :
    HasFPowerSeriesWithinAt f p s x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
hf : HasFPowerSeriesWithinAt f p univ x
⊢ HasFPowerSeriesWithinAt f p s x

Tactic:
apply hf.mono (subset_univ _)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
hf : HasFPowerSeriesAt f p x
⊢ HasFPowerSeriesWithinAt f p s x

Tactic:
rw [← hasFPowerSeriesWithinAt_univ] at hf

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
hf : HasFPowerSeriesWithinAt f p univ x
⊢ HasFPowerSeriesWithinAt f p s x
-- Mathlib/Algebra/Homology/Embedding/TruncGEHomology.lean
lemma quasiIso_truncGEMap_iff :
    QuasiIso (truncGEMap φ e) ↔ ∀ (i : ι) (i' : ι') (_ : e.f i = i'), QuasiIsoAt φ i'

Proof state:
case mp
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
this : ∀ (i : ι) (i' : ι'), e.f i = i' → (QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
⊢ (∀ (i : ι'), QuasiIsoAt (truncGEMap φ e) i) → ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'

Tactic:
intro h i i' hi

Result:
case mp
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
this : ∀ (i : ι) (i' : ι'), e.f i = i' → (QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι'), QuasiIsoAt (truncGEMap φ e) i
i : ι
i' : ι'
hi : e.f i = i'
⊢ QuasiIsoAt φ i'