harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem isDedekindDomainInv_iff [Algebra A K] [IsFractionRing A K] :
    IsDedekindDomainInv A ↔ ∀ I ≠ (⊥ : FractionalIdeal A⁰ K), I * I⁻¹ = 1

Proof state:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K := mapEquiv (FractionRing.algEquiv A K)
⊢ IsDedekindDomainInv A ↔ ∀ (I : FractionalIdeal A⁰ K), I ≠ ⊥ → I * I⁻¹ = 1

Tactic:
refine h.toEquiv.forall_congr (fun {x} => ?_)

Result:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K := mapEquiv (FractionRing.algEquiv A K)
x : FractionalIdeal A⁰ (FractionRing A)
⊢ x ≠ ⊥ → x * x⁻¹ = 1 ↔ h.toEquiv x ≠ ⊥ → h.toEquiv x * (h.toEquiv x)⁻¹ = 1

Proof state:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K := mapEquiv (FractionRing.algEquiv A K)
x : FractionalIdeal A⁰ (FractionRing A)
⊢ x ≠ ⊥ → x * x⁻¹ = 1 ↔ h.toEquiv x ≠ ⊥ → h.toEquiv x * (h.toEquiv x)⁻¹ = 1

Tactic:
rw [← h.toEquiv.apply_eq_iff_eq]

Result:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K := mapEquiv (FractionRing.algEquiv A K)
x : FractionalIdeal A⁰ (FractionRing A)
⊢ x ≠ ⊥ → h.toEquiv (x * x⁻¹) = h.toEquiv 1 ↔ h.toEquiv x ≠ ⊥ → h.toEquiv x * (h.toEquiv x)⁻¹ = 1

Proof state:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ IsDedekindDomainInv A ↔ ∀ (I : FractionalIdeal A⁰ K), I ≠ ⊥ → I * I⁻¹ = 1

Tactic:
let h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K :=
  FractionalIdeal.mapEquiv (FractionRing.algEquiv A K)

Result:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K := mapEquiv (FractionRing.algEquiv A K)
⊢ IsDedekindDomainInv A ↔ ∀ (I : FractionalIdeal A⁰ K), I ≠ ⊥ → I * I⁻¹ = 1

Proof state:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
h : FractionalIdeal A⁰ (FractionRing A) ≃+* FractionalIdeal A⁰ K := mapEquiv (FractionRing.algEquiv A K)
x : FractionalIdeal A⁰ (FractionRing A)
⊢ x ≠ ⊥ → h.toEquiv (x * x⁻¹) = h.toEquiv 1 ↔ h.toEquiv x ≠ ⊥ → h.toEquiv x * (h.toEquiv x)⁻¹ = 1

Tactic:
simp [h, IsDedekindDomainInv]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem abs_re_le_norm (z : K) : |re z| ≤ ‖z‖

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ re z * re z ≤ normSq z

Tactic:
apply re_sq_le_normSq

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ |re z| ≤ ‖z‖

Tactic:
rw [mul_self_le_mul_self_iff (abs_nonneg _) (norm_nonneg _), abs_mul_abs_self, mul_self_norm]

Result:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ re z * re z ≤ normSq z
-- Mathlib/Algebra/Homology/Embedding/Basic.lean
lemma rel_iff [e.IsRelIff] (i₁ i₂ : ι) : c'.Rel (e.f i₁) (e.f i₂) ↔ c.Rel i₁ i₂

Proof state:
case mp
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i₁ i₂ : ι
⊢ c'.Rel (e.f i₁) (e.f i₂) → c.Rel i₁ i₂

Tactic:
apply IsRelIff.rel'

Result:
no goals

Proof state:
case mpr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i₁ i₂ : ι
⊢ c.Rel i₁ i₂ → c'.Rel (e.f i₁) (e.f i₂)

Tactic:
exact e.rel

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i₁ i₂ : ι
⊢ c'.Rel (e.f i₁) (e.f i₂) ↔ c.Rel i₁ i₂

Tactic:
constructor

Result:
case mp
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i₁ i₂ : ι
⊢ c'.Rel (e.f i₁) (e.f i₂) → c.Rel i₁ i₂

case mpr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i₁ i₂ : ι
⊢ c.Rel i₁ i₂ → c'.Rel (e.f i₁) (e.f i₂)
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem _root_.exists_prime_orderOf_dvd_card {G : Type*} [Group G] [Fintype G] (p : ℕ)
    [hp : Fact p.Prime] (hdvd : p ∣ Fintype.card G) : ∃ x : G, orderOf x = p

Proof state:
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v => VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
⊢ ∃ x, orderOf x = p

Tactic:
have hf2 : ∀ j k v, f k (f j v) = f (j + k) v := fun j k v =>
  VectorsProdEqOne.rotate_rotate v j k

Result:
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v => VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
⊢ ∃ x, orderOf x = p
-- Mathlib/Data/Part.lean
theorem assert_pos {p : Prop} {f : p → Part α} (h : p) : assert p f = f h

Proof state:
case mk
α : Type u_1
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ HEq (fun ha => get✝ ⋯) get✝

Tactic:
apply Function.hfunext

Result:
case mk.hα
α : Type u_1
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ (∃ (h : p), (f h).Dom) = Dom✝

case mk.h
α : Type u_1
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ ∀ (a : ∃ (h : p), (f h).Dom) (a' : Dom✝), HEq a a' → HEq (get✝ ⋯) (get✝ a')

Proof state:
α : Type u_1
p : Prop
f : p → Part α
h : p
⊢ { Dom := ∃ (h : p), (f h).Dom, get := fun ha => (f ⋯).get ⋯ } = f h

Tactic:
cases h' : f h

Result:
case mk
α : Type u_1
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ { Dom := ∃ (h : p), (f h).Dom, get := fun ha => (f ⋯).get ⋯ } = { Dom := Dom✝, get := get✝ }

Proof state:
α : Type u_1
p : Prop
f : p → Part α
h : p
⊢ assert p f = f h

Tactic:
dsimp [assert]

Result:
α : Type u_1
p : Prop
f : p → Part α
h : p
⊢ { Dom := ∃ (h : p), (f h).Dom, get := fun ha => (f ⋯).get ⋯ } = f h

Proof state:
case mk.h
α : Type u_1
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ ∀ (a : ∃ (h : p), (f h).Dom) (a' : Dom✝), HEq a a' → HEq (get✝ ⋯) (get✝ a')

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ { Dom := ∃ (h : p), (f h).Dom, get := fun ha => (f ⋯).get ⋯ } = { Dom := Dom✝, get := get✝ }

Tactic:
simp only [h', mk.injEq, h, exists_prop_of_true, true_and]

Result:
case mk
α : Type u_1
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ HEq (fun ha => get✝ ⋯) get✝

Proof state:
case mk.hα
α : Type u_1
p : Prop
f : p → Part α
h : p
Dom✝ : Prop
get✝ : Dom✝ → α
h' : f h = { Dom := Dom✝, get := get✝ }
⊢ (∃ (h : p), (f h).Dom) = Dom✝

Tactic:
simp only [h, h', exists_prop_of_true]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma exists_between_coe_real {x z : EReal} (h : x < z) : ∃ y : ℝ, x < y ∧ y < z

Proof state:
case intro.intro.h_top
x z : EReal
h : x < z
ha₁ : x < ⊤
ha₂ : ⊤ < z
⊢ ∃ y, x < ↑y ∧ ↑y < z

Tactic:
exact (not_top_lt ha₂).elim

Result:
no goals

Proof state:
case intro.intro.h_real
x z : EReal
h : x < z
a₀ : ℝ
ha₁ : x < ↑a₀
ha₂ : ↑a₀ < z
⊢ ∃ y, x < ↑y ∧ ↑y < z

Tactic:
exact ⟨a₀, ha₁, ha₂⟩

Result:
no goals

Proof state:
case intro.intro
x z : EReal
h : x < z
a : EReal
ha₁ : x < a
ha₂ : a < z
⊢ ∃ y, x < ↑y ∧ ↑y < z

Tactic:
induction a with
| h_bot => exact (not_lt_bot ha₁).elim
| h_real a₀ => exact ⟨a₀, ha₁, ha₂⟩
| h_top => exact (not_top_lt ha₂).elim

Result:
no goals

Proof state:
x z : EReal
h : x < z
⊢ ∃ y, x < ↑y ∧ ↑y < z

Tactic:
obtain ⟨a, ha₁, ha₂⟩ := exists_between h

Result:
case intro.intro
x z : EReal
h : x < z
a : EReal
ha₁ : x < a
ha₂ : a < z
⊢ ∃ y, x < ↑y ∧ ↑y < z

Proof state:
case intro.intro.h_bot
x z : EReal
h : x < z
ha₁ : x < ⊥
ha₂ : ⊥ < z
⊢ ∃ y, x < ↑y ∧ ↑y < z

Tactic:
exact (not_lt_bot ha₁).elim

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Comap.lean
lemma comap_comap (hf' : ∀ s, MeasurableSet s → MeasurableSet (f '' s)) (hg : Injective g)
    (hg' : ∀ s, MeasurableSet s → MeasurableSet (g '' s)) (μ : Measure γ) :
    comap f (comap g μ) = comap (g ∘ f) μ

Proof state:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
g : β → γ
hf' : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
hg : Injective g
hg' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (g '' s)
μ : Measure γ
hf : ¬Injective f
⊢ comap f (comap g μ) = comap (g ∘ f) μ

Tactic:
rw [comap, dif_neg <| mt And.left hf, comap, dif_neg fun h ↦ hf h.1.of_comp]

Result:
no goals

Proof state:
case pos.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
g : β → γ
hf' : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
hg : Injective g
hg' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (g '' s)
μ : Measure γ
hf : Injective f
s : Set α
hs : MeasurableSet s
⊢ (comap f (comap g μ)) s = (comap (g ∘ f) μ) s

Tactic:
rw [comap_apply _ hf hf' _ hs, comap_apply _ hg hg' _ (hf' _ hs),
  comap_apply _ (hg.comp hf) (fun t ht ↦ image_comp g f _ ▸ hg' _ <| hf' _ ht) _ hs, image_comp]

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
g : β → γ
hf' : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
hg : Injective g
hg' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (g '' s)
μ : Measure γ
hf : Injective f
⊢ comap f (comap g μ) = comap (g ∘ f) μ

Tactic:
ext s hs

Result:
case pos.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
g : β → γ
hf' : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
hg : Injective g
hg' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (g '' s)
μ : Measure γ
hf : Injective f
s : Set α
hs : MeasurableSet s
⊢ (comap f (comap g μ)) s = (comap (g ∘ f) μ) s

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
g : β → γ
hf' : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
hg : Injective g
hg' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (g '' s)
μ : Measure γ
⊢ comap f (comap g μ) = comap (g ∘ f) μ

Tactic:
by_cases hf : Injective f

Result:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
g : β → γ
hf' : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
hg : Injective g
hg' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (g '' s)
μ : Measure γ
hf : Injective f
⊢ comap f (comap g μ) = comap (g ∘ f) μ

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β
g : β → γ
hf' : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)
hg : Injective g
hg' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (g '' s)
μ : Measure γ
hf : ¬Injective f
⊢ comap f (comap g μ) = comap (g ∘ f) μ
-- Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
theorem map_smulₛₗ₂ (f : M →SL[ρ₁₂] F →SL[σ₁₂] G') (c : R) (x : M) (y : F) :
    f (c • x) y = ρ₁₂ c • f x y

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹¹ : SeminormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
R : Type u_5
𝕜₂ : Type u_6
𝕜' : Type u_7
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NontriviallyNormedField 𝕜₂
M : Type u_8
inst✝⁷ : TopologicalSpace M
σ₁₂ : 𝕜 →+* 𝕜₂
G' : Type u_9
inst✝⁶ : SeminormedAddCommGroup G'
inst✝⁵ : NormedSpace 𝕜₂ G'
inst✝⁴ : NormedSpace 𝕜' G'
inst✝³ : SMulCommClass 𝕜₂ 𝕜' G'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ρ₁₂ : R →+* 𝕜'
f : M →SL[ρ₁₂] F →SL[σ₁₂] G'
c : R
x : M
y : F
⊢ (f (c • x)) y = ρ₁₂ c • (f x) y

Tactic:
rw [f.map_smulₛₗ, smul_apply]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocDiv_wcovBy_toIcoDiv (a b : α) : toIocDiv hp a b ⩿ toIcoDiv hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a b ⩿ toIcoDiv hp a b

Tactic:
suffices toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b by
  rwa [wcovBy_iff_eq_or_covBy, ← Order.succ_eq_iff_covBy]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ ¬a ≡ b [PMOD p] ∨ a ≡ b [PMOD p]

Tactic:
exact em' _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b

Tactic:
rw [eq_comm, ← not_modEq_iff_toIcoDiv_eq_toIocDiv, eq_comm, ←
  modEq_iff_toIcoDiv_eq_toIocDiv_add_one]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ ¬a ≡ b [PMOD p] ∨ a ≡ b [PMOD p]

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
this : toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b
⊢ toIocDiv hp a b ⩿ toIcoDiv hp a b

Tactic:
rwa [wcovBy_iff_eq_or_covBy, ← Order.succ_eq_iff_covBy]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem IsPrimitive.primPart_eq {p : R[X]} (hp : p.IsPrimitive) : p.primPart = p

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : p.IsPrimitive
⊢ p.primPart = p

Tactic:
rw [← one_mul p.primPart, ← C_1, ← hp.content_eq_one, ← p.eq_C_content_mul_primPart]

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean
theorem contMDiffOn_model_symm : ContMDiffOn 𝓘(𝕜, E) I n I.symm (range I)

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
n : WithTop ℕ∞
⊢ ContMDiffOn 𝓘(𝕜, E) I n (↑I.symm) (range ↑I)

Tactic:
rw [contMDiffOn_iff]

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
n : WithTop ℕ∞
⊢ ContinuousOn (↑I.symm) (range ↑I) ∧
    ∀ (x : E) (y : H),
      ContDiffOn 𝕜 n (↑(extChartAt I y) ∘ ↑I.symm ∘ ↑(extChartAt 𝓘(𝕜, E) x).symm)
        ((extChartAt 𝓘(𝕜, E) x).target ∩
          ↑(extChartAt 𝓘(𝕜, E) x).symm ⁻¹' (range ↑I ∩ ↑I.symm ⁻¹' (extChartAt I y).source))

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
n : WithTop ℕ∞
x : E
y : H
⊢ ContDiffOn 𝕜 n (↑(extChartAt I y) ∘ ↑I.symm ∘ ↑(extChartAt 𝓘(𝕜, E) x).symm)
    ((extChartAt 𝓘(𝕜, E) x).target ∩ ↑(extChartAt 𝓘(𝕜, E) x).symm ⁻¹' (range ↑I ∩ ↑I.symm ⁻¹' (extChartAt I y).source))

Tactic:
simp only [mfld_simps]

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
n : WithTop ℕ∞
x : E
y : H
⊢ ContDiffOn 𝕜 n (↑I ∘ ↑I.symm) (range ↑I)

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
n : WithTop ℕ∞
x : E
y : H
⊢ ContDiffOn 𝕜 n (↑I ∘ ↑I.symm) (range ↑I)

Tactic:
exact contDiffOn_id.congr fun x' => I.right_inv

Result:
no goals

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
n : WithTop ℕ∞
⊢ ContinuousOn (↑I.symm) (range ↑I) ∧
    ∀ (x : E) (y : H),
      ContDiffOn 𝕜 n (↑(extChartAt I y) ∘ ↑I.symm ∘ ↑(extChartAt 𝓘(𝕜, E) x).symm)
        ((extChartAt 𝓘(𝕜, E) x).target ∩
          ↑(extChartAt 𝓘(𝕜, E) x).symm ⁻¹' (range ↑I ∩ ↑I.symm ⁻¹' (extChartAt I y).source))

Tactic:
refine ⟨I.continuousOn_symm, fun x y => ?_⟩

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
n : WithTop ℕ∞
x : E
y : H
⊢ ContDiffOn 𝕜 n (↑(extChartAt I y) ∘ ↑I.symm ∘ ↑(extChartAt 𝓘(𝕜, E) x).symm)
    ((extChartAt 𝓘(𝕜, E) x).target ∩ ↑(extChartAt 𝓘(𝕜, E) x).symm ⁻¹' (range ↑I ∩ ↑I.symm ⁻¹' (extChartAt I y).source))
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
theorem app_eq_appIso_inv_app_of_comp_eq {X Y U : Scheme.{u}} (f : Y ⟶ U) (g : U ⟶ X) (fg : Y ⟶ X)
    (H : fg = f ≫ g) [h : IsOpenImmersion g] (V : U.Opens) :
    f.app V = (g.appIso V).inv ≫ fg.app (g ''ᵁ V) ≫ Y.presheaf.map
      (eqToHom <| IsOpenImmersion.app_eq_invApp_app_of_comp_eq_aux f g fg H V).op

Proof state:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
fg : Y ⟶ X
H : fg = f ≫ g
h : IsOpenImmersion g
V : U.Opens
⊢ Scheme.Hom.app f V = (Scheme.Hom.appIso g V).inv ≫ Scheme.Hom.app fg (g ''ᵁ V) ≫ Y.presheaf.map (eqToHom ⋯).op

Tactic:
subst H

Result:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
⊢ Scheme.Hom.app f V = (Scheme.Hom.appIso g V).inv ≫ Scheme.Hom.app (f ≫ g) (g ''ᵁ V) ≫ Y.presheaf.map (eqToHom ⋯).op

Proof state:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
⊢ Scheme.Hom.app f V = (Scheme.Hom.appIso g V).inv ≫ Scheme.Hom.app (f ≫ g) (g ''ᵁ V) ≫ Y.presheaf.map (eqToHom ⋯).op

Tactic:
rw [Scheme.comp_app, Category.assoc, Scheme.Hom.appIso_inv_app_assoc, f.naturality_assoc,
  ← Functor.map_comp, ← op_comp, Quiver.Hom.unop_op, eqToHom_map, eqToHom_trans,
  eqToHom_op, eqToHom_refl, CategoryTheory.Functor.map_id, Category.comp_id]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem Left.mul_nonneg [PosMulMono α] (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a * b

Proof state:
α : Type u_3
a b : α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b

Tactic:
simpa only [mul_zero] using mul_le_mul_of_nonneg_left hb ha

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorBundle/Basic.lean
theorem ContMDiffWithinAt.change_section_trivialization {f : M → TotalSpace F E}
    (hp : ContMDiffWithinAt IM IB n (π F E ∘ f) s x)
    (hf : ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y ↦ (e (f y)).2) s x)
    (he : f x ∈ e.source) (he' : f x ∈ e'.source) :
    ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y ↦ (e' (f y)).2) s x

Proof state:
n : WithTop ℕ∞
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝²⁰ : NormedAddCommGroup EB
inst✝¹⁹ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹⁸ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹⁷ : TopologicalSpace B
inst✝¹⁶ : ChartedSpace HB B
EM : Type u_9
inst✝¹⁵ : NormedAddCommGroup EM
inst✝¹⁴ : NormedSpace 𝕜 EM
HM : Type u_10
inst✝¹³ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝¹² : TopologicalSpace M
inst✝¹¹ : ChartedSpace HM M
inst✝¹⁰ : (x : B) → AddCommMonoid (E x)
inst✝⁹ : (x : B) → Module 𝕜 (E x)
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : TopologicalSpace (TotalSpace F E)
inst✝⁵ : (x : B) → TopologicalSpace (E x)
inst✝⁴ : FiberBundle F E
inst✝³ : VectorBundle 𝕜 F E
inst✝² : ContMDiffVectorBundle n F E IB
e e' : Trivialization F TotalSpace.proj
inst✝¹ : MemTrivializationAtlas e
inst✝ : MemTrivializationAtlas e'
s : Set M
x : M
f : M → TotalSpace F E
hp : ContMDiffWithinAt IM IB n (TotalSpace.proj ∘ f) s x
hf : ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y => (↑e (f y)).2) s x
he : f x ∈ e.source
he' : f x ∈ e'.source
⊢ ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y => (↑e' (f y)).2) s x

Tactic:
rw [Trivialization.mem_source] at he he'

Result:
n : WithTop ℕ∞
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst✝²¹ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝²⁰ : NormedAddCommGroup EB
inst✝¹⁹ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝¹⁸ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹⁷ : TopologicalSpace B
inst✝¹⁶ : ChartedSpace HB B
EM : Type u_9
inst✝¹⁵ : NormedAddCommGroup EM
inst✝¹⁴ : NormedSpace 𝕜 EM
HM : Type u_10
inst✝¹³ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝¹² : TopologicalSpace M
inst✝¹¹ : ChartedSpace HM M
inst✝¹⁰ : (x : B) → AddCommMonoid (E x)
inst✝⁹ : (x : B) → Module 𝕜 (E x)
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : TopologicalSpace (TotalSpace F E)
inst✝⁵ : (x : B) → TopologicalSpace (E x)
inst✝⁴ : FiberBundle F E
inst✝³ : VectorBundle 𝕜 F E
inst✝² : ContMDiffVectorBundle n F E IB
e e' : Trivialization F TotalSpace.proj
inst✝¹ : MemTrivializationAtlas e
inst✝ : MemTrivializationAtlas e'
s : Set M
x : M
f : M → TotalSpace F E
hp : ContMDiffWithinAt IM IB n (TotalSpace.proj ∘ f) s x
hf : ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y => (↑e (f y)).2) s x
he : (f x).proj ∈ e.baseSet
he' : (f x).proj ∈ e'.baseSet
⊢ ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y => (↑e' (f y)).2) s x
-- Mathlib/GroupTheory/Perm/Support.lean
theorem one_lt_card_support_of_ne_one {f : Perm α} (h : f ≠ 1) : 1 < #f.support

Proof state:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
a : α
h : f (f a) = f a ∨ f a = a ∨ f a = a
⊢ f a = 1 a

Tactic:
rwa [apply_eq_iff_eq, or_self_iff, or_self_iff] at h

Result:
no goals

Proof state:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : ∀ (a b : α), f a = a ∨ f b = b ∨ a = b
a : α
⊢ f a = 1 a

Tactic:
specialize h (f a) a

Result:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
a : α
h : f (f a) = f a ∨ f a = a ∨ f a = a
⊢ f a = 1 a

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : ∀ (a b : α), f a = a ∨ f b = b ∨ a = b
⊢ f = 1

Tactic:
ext a

Result:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : ∀ (a b : α), f a = a ∨ f b = b ∨ a = b
a : α
⊢ f a = 1 a

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f ≠ 1
⊢ ∃ a b, ¬(f a = a ∨ f b = b ∨ a = b)

Tactic:
contrapose! h

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : ∀ (a b : α), f a = a ∨ f b = b ∨ a = b
⊢ f = 1

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f ≠ 1
⊢ 1 < #f.support

Tactic:
simp_rw [one_lt_card_iff, mem_support, ← not_or]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f ≠ 1
⊢ ∃ a b, ¬(f a = a ∨ f b = b ∨ a = b)
-- Mathlib/Topology/MetricSpace/ThickenedIndicator.lean
theorem thickenedIndicatorAux_le_one (δ : ℝ) (E : Set α) (x : α) :
    thickenedIndicatorAux δ E x ≤ 1

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
⊢ thickenedIndicatorAux δ E x ≤ 1

Tactic:
apply tsub_le_self (α := ℝ≥0∞)

Result:
no goals
-- Mathlib/Analysis/Complex/ReImTopology.lean
protected lemma TendstoUniformlyOn.re {f : ι → α → ℂ} {p : Filter ι} {g : α → ℂ} {K : Set α}
    (hf : TendstoUniformlyOn f g p K) :
    TendstoUniformlyOn (fun n x => (f n x).re) (fun y => (g y).re) p K

Proof state:
α : Type u_1
ι : Type u_2
f : ι → α → ℂ
p : Filter ι
g : α → ℂ
K : Set α
hf : TendstoUniformlyOn f g p K
⊢ TendstoUniformlyOn (fun n x => (f n x).re) (fun y => (g y).re) p K

Tactic:
apply UniformContinuous.comp_tendstoUniformlyOn uniformlyContinuous_re hf

Result:
no goals